diff options
Diffstat (limited to 'lib/hol/prompt.lem')
| -rw-r--r-- | lib/hol/prompt.lem | 12 |
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 |