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) -> 'a list -> ('rv, unit, 'e) Sail2_prompt_monad.monad
val iteri : (Nat_big_num.num -> 'a -> ('rv, unit, 'e) Sail2_prompt_monad.monad) -> 'a list -> ('rv, unit, 'e) Sail2_prompt_monad.monad
val iter : ('a -> ('rv, unit, 'e) Sail2_prompt_monad.monad) -> 'a list -> ('rv, unit, 'e) Sail2_prompt_monad.monad
val foreachM : 'a list -> 'vars -> ('a -> 'vars -> ('rv, 'vars, 'e) Sail2_prompt_monad.monad) -> ('rv, 'vars, 'e) Sail2_prompt_monad.monad
val foreachE : 'a list -> 'vars -> ('a -> 'vars -> ('e, 'vars) Either.either) -> ('e, 'vars) Either.either
val genlistM : (Nat_num.nat -> ('rv, 'a, 'e) Sail2_prompt_monad.monad) -> Nat_num.nat -> ('rv, 'a list, 'e) Sail2_prompt_monad.monad
val and_boolM : ('rv, bool, 'e) Sail2_prompt_monad.monad -> ('rv, bool, 'e) Sail2_prompt_monad.monad -> ('rv, bool, 'e) Sail2_prompt_monad.monad
val or_boolM : ('rv, bool, 'e) Sail2_prompt_monad.monad -> ('rv, bool, 'e) Sail2_prompt_monad.monad -> ('rv, bool, 'e) 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 -> ('rv, bool, 'e) Sail2_prompt_monad.monad
val bools_of_bits_nondet : 'rv Sail2_values.register_Value_class -> Sail2_values.bitU list -> ('rv, bool list, 'e) Sail2_prompt_monad.monad
val of_bits_fail : 'a Sail2_values.bitvector_class -> Sail2_values.bitU list -> ('rv, 'a, 'e) Sail2_prompt_monad.monad
val mword_nondet : 'a Lem_pervasives_extra.size_class -> 'rv Sail2_values.register_Value_class -> unit -> ('rv, Lem.mword, 'e) Sail2_prompt_monad.monad
val whileM : 'vars -> ('vars -> ('rv, bool, 'e) Sail2_prompt_monad.monad) -> ('vars -> ('rv, 'vars, 'e) Sail2_prompt_monad.monad) -> ('rv, 'vars, 'e) Sail2_prompt_monad.monad
val untilM : 'vars -> ('vars -> ('rv, bool, 'e) Sail2_prompt_monad.monad) -> ('vars -> ('rv, 'vars, 'e) Sail2_prompt_monad.monad) -> ('rv, 'vars, 'e) Sail2_prompt_monad.monad
val choose_bools : 'rv Sail2_values.register_Value_class -> string -> Nat_num.nat -> ('rv, 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 -> ('rv, 'a, 'e) Sail2_prompt_monad.monad
val choose_from_list : 'rv Sail2_values.register_Value_class -> string -> 'a list -> ('rv, 'a, 'e) Sail2_prompt_monad.monad
val choose_int_in_range : 'rv Sail2_values.register_Value_class -> string -> Nat_big_num.num -> Nat_big_num.num -> ('rv, Nat_big_num.num, 'e) Sail2_prompt_monad.monad
val choose_nat : 'rv Sail2_values.register_Value_class -> string -> ('rv, Nat_big_num.num, 'e) Sail2_prompt_monad.monad
val internal_pick : 'rv Sail2_values.register_Value_class -> 'a list -> ('rv, 'a, 'e) Sail2_prompt_monad.monad
OCaml

Innovation. Community. Security.