fact: Definition desugarNonNullArguments (specs: list FULL_SPEC_CASE.t) (m:METHOD.t) : list FULL_SPEC_CASE.t := let reqs := paramsNonNullRequires (METHODSIGNATURE.parameters (METHOD.signature m)) in let defaultCase := GENERIC_SPEC_CASE.Build_t nil nil reqs (inl _ nil) in let defaultSpecs := FULL_SPEC_CASE.Build_t lightweight None false false defaultCase in match reqs, specs with | nil, _ => specs | _, nil => defaultSpecs :: nil | _, _ => map (fun s => addHeaders s reqs) 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)