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 let inline foreachM = foreachS let inline whileM = whileS let inline untilM = untilS let inline and_boolM = and_boolS let inline or_boolM = or_boolS