Added condo2.

PLTools · May 11, 2024 · 2026663 · 2026663
1 parent 4215a06
commit 2026663
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 0 deletions.
diff --git a/src/core/Core.ml b/src/core/Core.ml
@@ -497,6 +497,12 @@ let (?|) gs st =
 
 let conde = (?|)
 
+let condo2 a b st =
+  let st = State.new_scope st in
+  match Stream.msplit @@ a st with
+  | Some (a, b) -> Stream.cons a b
+  | None -> b st
+
 let call_fresh f st =
   let x = State.fresh st in
   f x st

diff --git a/src/core/Core.mli b/src/core/Core.mli
@@ -82,6 +82,8 @@ val (|||) : goal -> goal -> goal
 *)
 val (?|) : goal list -> goal
 
+val condo2 : goal -> goal -> goal
+
 (** [conde] is a synonym for [?|] *)
 val conde : goal list -> goal