diff options
| author | Thomas Bauereiss | 2019-02-08 18:04:51 +0000 |
|---|---|---|
| committer | Thomas Bauereiss | 2019-02-08 18:19:47 +0000 |
| commit | ad868ef0ad22a78021a5de91073416f69e8163d3 (patch) | |
| tree | 3b41a9dfd5d532e6a34f75e1e57ae42d6138b80a /lib/hol/sail2_prompt.lem | |
| parent | fc5558d2b62365ea65818947780081dad74d4526 (diff) | |
Add missing functions to HOL monad wrapper
Also make the rewriter keep failed assertions in output when pruning
blocks.
Diffstat (limited to 'lib/hol/sail2_prompt.lem')
| -rw-r--r-- | lib/hol/sail2_prompt.lem | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/lib/hol/sail2_prompt.lem b/lib/hol/sail2_prompt.lem index 674d4e34..3107d3a5 100644 --- a/lib/hol/sail2_prompt.lem +++ b/lib/hol/sail2_prompt.lem @@ -4,12 +4,13 @@ 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 bool_of_bitU_fail = Sail2_state.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 choose msg xs = chooseS xs let inline internal_pick = internal_pickS let inline foreachM = foreachS |