Add Boolean short-circuiting to state monad

1 files changed, 6 insertions, 0 deletions

diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem
index 6bc304a8..f69f59c1 100644
--- a/src/gen_lib/state.lem
+++ b/src/gen_lib/state.lem
@@ -28,6 +28,12 @@ end
 
 declare {isabelle} termination_argument foreachS = automatic
 
+val and_boolS : forall 'rv 'e. monadS 'rv bool 'e -> monadS 'rv bool 'e -> monadS 'rv bool 'e
+let and_boolS l r = l >>$= (fun l -> if l then r else returnS false)
+
+val or_boolS : forall 'rv 'e. monadS 'rv bool 'e -> monadS 'rv bool 'e -> monadS 'rv bool 'e
+let or_boolS l r = l >>$= (fun l -> if l then returnS true else r)
+
 val bool_of_bitU_fail : forall 'rv 'e. bitU -> monadS 'rv bool 'e
 let bool_of_bitU_fail = function
   | B0 -> returnS false