aboutsummaryrefslogtreecommitdiff
path: root/engine/logic_monad.ml
diff options
context:
space:
mode:
Diffstat (limited to 'engine/logic_monad.ml')
-rw-r--r--engine/logic_monad.ml8
1 files changed, 8 insertions, 0 deletions
diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml
index 79bf48acdd..c88de133d4 100644
--- a/engine/logic_monad.ml
+++ b/engine/logic_monad.ml
@@ -215,6 +215,14 @@ struct
let modify f =
{ iolist = fun s nil cons -> cons () (f s) nil }
+ (** Exception manipulation *)
+
+ let interleave src dst m =
+ { iolist = fun s nil cons ->
+ m.iolist s (fun e1 -> nil (src e1))
+ (fun x s next -> cons x s (fun e2 -> next (dst e2)))
+ }
+
(** List observation *)
let once m =