package libsail

  1. Overview
  2. Docs
val iter_aux : Nat_big_num.num -> (Nat_big_num.num -> 'a -> ('rv, unit, 'e) Sail2_prompt_monad.monad) -> 'b list -> ('rv0, unit, 'e0) Sail2_prompt_monad.monad
val iteri : (Nat_big_num.num -> 'a -> ('rv, unit, 'e) Sail2_prompt_monad.monad) -> 'a list -> ('rv0, unit, 'e0) Sail2_prompt_monad.monad
val iter : ('a -> ('rv, unit, 'e) Sail2_prompt_monad.monad) -> 'b list -> ('rv0, unit, 'e0) Sail2_prompt_monad.monad
val foreachM : 'a list -> 'vars -> ('b -> 'vars0 -> ('rv, 'vars1, 'e) Sail2_prompt_monad.monad) -> ('rv0, 'vars2, 'e0) Sail2_prompt_monad.monad
val foreachE : 'a list -> 'vars -> ('b -> 'vars0 -> ('e, 'vars1) Either.either) -> ('e, 'vars2) Either.either
val genlistM : (Nat_num.nat -> ('rv, 'a, 'e) Sail2_prompt_monad.monad) -> Nat_num.nat -> ('rv0, 'a0 list, 'e0) Sail2_prompt_monad.monad
val and_boolM : ('rv, bool, 'e) Sail2_prompt_monad.monad -> ('rv, bool, 'e) Sail2_prompt_monad.monad -> ('rv0, bool, 'e0) Sail2_prompt_monad.monad
val or_boolM : ('rv, bool, 'e) Sail2_prompt_monad.monad -> ('rv, bool, 'e) Sail2_prompt_monad.monad -> ('rv0, bool, 'e0) Sail2_prompt_monad.monad
val bool_of_bitU_fail : Sail2_values.bitU -> ('rv, bool, 'e) Sail2_prompt_monad.monad
val bool_of_bitU_nondet : 'rv Sail2_values.register_Value_class -> Sail2_values.bitU -> ('rv0, bool, 'e) Sail2_prompt_monad.monad
val bools_of_bits_nondet : 'rv Sail2_values.register_Value_class -> Sail2_values.bitU list -> ('rv0, bool list, 'e) Sail2_prompt_monad.monad
val of_bits_fail : 'a Sail2_values.bitvector_class -> Sail2_values.bitU list -> ('rv, 'a0, 'e) Sail2_prompt_monad.monad
val whileM : 'vars -> ('vars0 -> ('rv, bool, 'e) Sail2_prompt_monad.monad) -> ('vars1 -> ('rv0, 'vars2, 'e0) Sail2_prompt_monad.monad) -> ('rv1, 'vars3, 'e1) Sail2_prompt_monad.monad
val untilM : 'vars -> ('vars0 -> ('rv, bool, 'e) Sail2_prompt_monad.monad) -> ('vars1 -> ('rv0, 'vars2, 'e0) Sail2_prompt_monad.monad) -> ('rv1, 'vars3, 'e1) Sail2_prompt_monad.monad
val choose_bools : 'rv Sail2_values.register_Value_class -> string -> Nat_num.nat -> ('rv0, bool list, 'e) Sail2_prompt_monad.monad
val choose_bitvector : 'a Sail2_values.bitvector_class -> 'rv Sail2_values.register_Value_class -> string -> Nat_num.nat -> ('rv0, 'a0, 'e) Sail2_prompt_monad.monad
val choose_from_list : 'rv Sail2_values.register_Value_class -> string -> 'a list -> ('rv0, 'a0, 'e) Sail2_prompt_monad.monad
val choose_nat : 'rv Sail2_values.register_Value_class -> string -> ('rv0, Nat_big_num.num, 'e) Sail2_prompt_monad.monad
val internal_pick : 'rv Sail2_values.register_Value_class -> 'a list -> ('rv0, 'a0, 'e) Sail2_prompt_monad.monad