fact: Fixpoint clausesMap (f : list MethodSpecClause -> list MethodSpecClause) (case : GENERIC_SPEC_CASE.t) : GENERIC_SPEC_CASE.t := let (fvd,ovd,sh,body) := case in match body with | inl clauses => GENERIC_SPEC_CASE.Build_t fvd ovd sh (inl _ (f clauses)) | inr nested0 => let nested1 := map (clausesMap f) nested0 in GENERIC_SPEC_CASE.Build_t fvd ovd sh (inr _ nested1) end.
imports: JML(Prelude) Coq(ZArith) Coq(Bool) Coq(List) JML(TaggedList) JML(ListHelpers) JML(ListFunctions) JML(OptionHelpers) JML(JMLProgramPlusImpl) JML(JMLFull2Basic) JML(JMLExpressionNotations)