fact: Definition mergeInvariants (invs:list INVARIANT.t) : INVARIANT.t := let and := BinaryCondBoolExpr ConditionalAnd in let lPred := map INVARIANT.pred invs in INVARIANT.Build_t (fold_right and true'%jml lPred) Public false false.
imports: JML(Prelude) Coq(ZArith) Coq(Bool) Coq(List) JML(TaggedList) JML(ListHelpers) JML(ListFunctions) JML(OptionHelpers) JML(JMLProgramPlusImpl) JML(JMLFull2Basic) JML(JMLExpressionNotations)