From a29c35cee2710540fc4e0465cfd2bc08835c12f8 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 7 May 2015 16:53:03 +0200 Subject: Adding a primitive to the tactic monad to modify the exceptional content. --- engine/logic_monad.ml | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'engine/logic_monad.ml') diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml index 79bf48acd..c88de133d 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 = -- cgit v1.2.3