From c3f3642dfa5647685ae3dea86beeef8abc27f026 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Fri, 4 May 2018 17:44:07 +0100
Subject: Support short-circuiting of Boolean expressions in Lem

---
 src/gen_lib/prompt.lem | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'src/gen_lib')

diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem
index de683047..830f2350 100644
--- a/src/gen_lib/prompt.lem
+++ b/src/gen_lib/prompt.lem
@@ -38,6 +38,12 @@ end
 
 declare {isabelle} termination_argument foreachM = automatic
 
+val and_boolM : forall 'rv 'e. monad 'rv bool 'e -> monad 'rv bool 'e -> monad 'rv bool 'e
+let and_boolM l r = l >>= (fun l -> if l then r else return false)
+
+val or_boolM : forall 'rv 'e. monad 'rv bool 'e -> monad 'rv bool 'e -> monad 'rv bool 'e
+let or_boolM l r = l >>= (fun l -> if l then return true else r)
+
 val bool_of_bitU_fail : forall 'rv 'e. bitU -> monad 'rv bool 'e
 let bool_of_bitU_fail = function
   | B0 -> return false
-- 
cgit v1.2.3