HOL script generation for library and CHERI

(still needs some Lem work on types before it will be useful)

1 files changed, 12 insertions, 0 deletions

diff --git a/lib/hol/prompt.lem b/lib/hol/prompt.lem
new file mode 100644
index 00000000..a04e0a0a
--- /dev/null
+++ b/lib/hol/prompt.lem
@@ -0,0 +1,12 @@
+open import Prompt_monad
+open import State_monad
+open import State
+
+let inline undefined_bool = undefined_boolS
+let inline bool_of_bitU_oracle = bool_of_bitU_oracleS
+let inline bool_of_bitU_fail = bool_of_bitU_fail
+let inline bools_of_bits_oracle = bools_of_bits_oracleS
+let inline of_bits_oracle = of_bits_oracleS
+let inline of_bits_fail = of_bits_failS
+let inline mword_oracle = mword_oracleS
+let inline reg_deref = read_regS