fact: Definition desugarEmptySpecification (specs:list FULL_SPEC_CASE.t) (m:METHOD.t) (enc:TYPEDEF.t) : list FULL_SPEC_CASE.t := let req := match METHOD.override m with | None => requiresSH false \not_specified%jml | Some _ => requiresSH false (: false' :)%jml end in let defaultCase := GENERIC_SPEC_CASE.Build_t nil nil (req::nil) (inl _ nil) in let defaultSpecs := FULL_SPEC_CASE.Build_t lightweight None false false defaultCase in match METHOD.isImplicitDefaultConstructor m, isEmptySpecification specs with | true, _ => (implicitCtorDefaultSpecs enc) :: nil | false, true => defaultSpecs :: nil | false, false => specs end.
imports: JML(Prelude) Coq(ZArith) Coq(Bool) Coq(List) JML(TaggedList) JML(ListHelpers) JML(ListFunctions) JML(OptionHelpers) JML(JMLProgramPlusImpl) JML(JMLFull2Basic) JML(JMLExpressionNotations)