blob: a04e0a0aafcd7a7db7bd50f7277f8ac87a3c5b20 (
plain)
1
2
3
4
5
6
7
8
9
10
11
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
|
