fact: Definition mergeSignals (l0:list (Param * optional Expression)) : option (Param * optional Expression) := let snd' := snd (A := Param) (B := optional Expression) in let l1 := map snd' l0 in match mergeEnsures l1 with | None => None | Some oe => Some (Exception_e, oe) end.
imports: JML(Prelude) Coq(ZArith) Coq(Bool) Coq(List) JML(TaggedList) JML(ListHelpers) JML(ListFunctions) JML(OptionHelpers) JML(JMLProgramPlusImpl) JML(JMLFull2Basic) JML(JMLExpressionNotations)