summaryrefslogtreecommitdiff
path: root/lib/hol/sail2_prompt.lem
blob: 3107d3a5ed8061e3770ef0aae943fc1d18d1b6c4 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
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 = 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
let inline whileM = whileS
let inline untilM = untilS
let inline and_boolM = and_boolS
let inline or_boolM = or_boolS