fact: Definition loopAnnotationDecl (lbl:Label) (annotations:list LOOP_ANNOTATION_TAG.data) : LOOP_ANNOTATION.t := let invs0 := LOOP_ANNOTATION_TAG.filterTag INVARIANT_TAG annotations in let invsRed0 := LOOP_ANNOTATION_TAG.filterTag INVARIANT_REDUNDANTLY_TAG annotations in let vars0 := LOOP_ANNOTATION_TAG.filterTag VARIANT_TAG annotations in let varsRed0 := LOOP_ANNOTATION_TAG.filterTag VARIANT_REDUNDANTLY_TAG annotations in let optionalAnd := liftOptional2 (BinaryCondBoolExpr ConditionalAnd) in let SpecifiedE := Specified (A := Expression) in let invs1 := fold_left1 optionalAnd (map SpecifiedE invs0) NotSpecified in let invsRed1 := fold_left1 optionalAnd (map SpecifiedE invsRed0) NotSpecified in let vars1 := map (rewriteVariant lbl) vars0 in let varsRed1 := map (rewriteVariant lbl) varsRed0 in let vars2 := fold_left1 optionalAnd (map SpecifiedE vars1) NotSpecified in let varsRed2 := fold_left1 optionalAnd (map SpecifiedE varsRed1) NotSpecified in LOOP_ANNOTATION.Build_t (optionalAnd invs1 vars2) (optionalAnd invsRed1 varsRed2) invs0 invsRed0 vars0 varsRed0.
imports: JML(Prelude) Coq(ZArith) Coq(Bool) Coq(List) JML(TaggedList) JML(ListHelpers) JML(ListFunctions) JML(OptionHelpers) JML(JMLProgramPlusImpl) JML(JMLFull2Basic) JML(JMLExpressionNotations)