summaryrefslogtreecommitdiff
path: root/lib/hol/sail2_prompt.lem
diff options
context:
space:
mode:
authorBrian Campbell2018-07-10 14:05:36 +0100
committerBrian Campbell2018-07-10 14:06:48 +0100
commitadadda8dfc80d0b7e6a967ceeda98624198800c1 (patch)
treecf12fc33403c821d78faa0883b26466f205f2e44 /lib/hol/sail2_prompt.lem
parentf652ae23b6cbaa3d70ae38f8942d6ae61af2c1d6 (diff)
Update HOL setup
Diffstat (limited to 'lib/hol/sail2_prompt.lem')
-rw-r--r--lib/hol/sail2_prompt.lem19
1 files changed, 19 insertions, 0 deletions
diff --git a/lib/hol/sail2_prompt.lem b/lib/hol/sail2_prompt.lem
new file mode 100644
index 00000000..674d4e34
--- /dev/null
+++ b/lib/hol/sail2_prompt.lem
@@ -0,0 +1,19 @@
+open import Sail2_prompt_monad
+open import Sail2_state_monad
+open import Sail2_state
+
+let inline undefined_bool = undefined_boolS
+let inline bool_of_bitU_nondet = bool_of_bitU_nondetS
+let inline bool_of_bitU_fail = bool_of_bitU_fail
+let inline bools_of_bits_nondet = bools_of_bits_nondetS
+let inline of_bits_nondet = of_bits_nondetS
+let inline of_bits_fail = of_bits_failS
+let inline mword_nondet = mword_nondetS
+let inline reg_deref = read_regS
+let inline internal_pick = internal_pickS
+
+let inline foreachM = foreachS
+let inline whileM = whileS
+let inline untilM = untilS
+let inline and_boolM = and_boolS
+let inline or_boolM = or_boolS