fact: Definition zeroArgCtor (enc:TYPEDEF.t) : option METHOD.t := let fix zeroArgCtorRec (l:list METHOD.t) : option METHOD.t := match l with | m::ms => match METHOD.kind m, METHODSIGNATURE.parameters (METHOD.signature m) with | Constructor, nil => Some m | _, _ => zeroArgCtorRec ms end | nil => None end in zeroArgCtorRec (TYPEDEF.methods enc).
imports: JML(Prelude) Coq(ZArith) Coq(Bool) Coq(List) JML(TaggedList) JML(ListHelpers) JML(ListFunctions) JML(OptionHelpers) JML(JMLProgramPlusImpl) JML(JMLFull2Basic) JML(JMLExpressionNotations)