You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copy file name to clipboardExpand all lines: src/smtml/expr_intf.ml
+7-3Lines changed: 7 additions & 3 deletions
Original file line number
Diff line number
Diff line change
@@ -554,11 +554,15 @@ module type S = sig
554
554
moduleF64 : Constructors_intf.Infixwithtype elt :=floatandtypet := t
555
555
end
556
556
557
-
(** {1. Simplifications bis} *)
557
+
(** {1 Simplifications bis} *)
558
558
559
-
(** [split_conjunctions e] when [e] is ((P & Q) & R) is { P; Q; R }. That is, it splits an expressions into a set of subformulas whose conjunctions is equivalent to the original expression. *)
559
+
(** [split_conjunctions e] when [e] is ((P & Q) & R) is [{ P; Q; R }]. That
560
+
is, it splits an expressions into a set of subformulas whose conjunctions
561
+
is equivalent to the original expression. *)
560
562
valsplit_conjunctions : t -> Set.t
561
563
562
-
(** [split_disjunctions e] when [e] is ((P || Q) || R) is { P; Q; R } That is, it splits an expressions into a set of subformulas whose disjunctions is equivalent to the original expression.*)
564
+
(** [split_disjunctions e] when [e] is ((P || Q) || R) is [{ P; Q; R }] That
565
+
is, it splits an expressions into a set of subformulas whose disjunctions
0 commit comments