summaryrefslogtreecommitdiff
path: root/src/gen_lib/prompt.lem
diff options
context:
space:
mode:
authorJon French2018-05-10 12:49:38 +0100
committerJon French2018-05-10 12:49:38 +0100
commit443601a0d19907d95ed604a68403403d25ceaf73 (patch)
tree289fa06f0583f4a2d1baec471ddc59b6ee4453e8 /src/gen_lib/prompt.lem
parent00c946d24c7f3f1cd9d5f6ef4798b72a2f7c3c16 (diff)
parent839f239f01ce3ecb4fe91a3f542d194591bc1650 (diff)
Merge branch 'sail2' into mappings
Diffstat (limited to 'src/gen_lib/prompt.lem')
-rw-r--r--src/gen_lib/prompt.lem6
1 files changed, 6 insertions, 0 deletions
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