fact: Definition mergeCallable (l:list (optional CallableList)) : option (optional CallableList) := let merge2 (cl1 cl2:CallableList) : CallableList := match cl1, cl2 with | METHODSPEC.EveryMethod, _ | _, METHODSPEC.EveryMethod => METHODSPEC.EveryMethod | METHODSPEC.These l1, METHODSPEC.These l2 => METHODSPEC.These (app l1 l2) end in match l with | nil => None | _ => Some (fold_left1 (liftOptional2 merge2) l NotSpecified) end.
imports: JML(Prelude) Coq(ZArith) Coq(Bool) Coq(List) JML(TaggedList) JML(ListHelpers) JML(ListFunctions) JML(OptionHelpers) JML(JMLProgramPlusImpl) JML(JMLFull2Basic) JML(JMLExpressionNotations)