package lem

  1. Overview
  2. Docs
val pair_equal : ('a -> 'b -> bool) -> ('c -> 'd -> bool) -> ('a * 'c) -> ('b * 'd) -> bool
val pair_swap : ('a * 'b) -> 'b * 'a
val curry : (('a * 'b) -> 'c) -> 'a -> 'b -> 'c
val uncurry : ('a -> 'b -> 'c) -> ('a * 'b) -> 'c
val orderingIsLess : int -> bool
val orderingIsGreater : int -> bool
val orderingIsEqual : int -> bool
val ordering_cases : int -> 'a -> 'a -> 'a -> 'a
val orderingEqual : int -> int -> bool
val list_null : 'a list -> bool
val lexicographic_compare : ('a -> 'b -> int) -> 'a list -> 'b list -> int
val lexicographic_less : ('a -> 'b -> bool) -> ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
val lexicographic_less_eq : ('a -> 'b -> bool) -> ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
val list_index : 'a list -> int -> 'a option
val is_none : 'a option -> bool
val is_some : 'a option -> bool
val option_case : 'a -> ('b -> 'a) -> 'b option -> 'a
val option_default : 'a -> 'a option -> 'a
val option_map : ('a -> 'b) -> 'a option -> 'b option
val option_bind : 'a option -> ('a -> 'b option) -> 'b option
val option_equal : ('a -> 'b -> bool) -> 'a option -> 'b option -> bool
val plus_float : float -> float -> float
val minus_float : float -> float -> float
val mult_float : float -> float -> float
val div_float : float -> float -> float
val pow_float : float -> float -> float
val pow_float_int : float -> int -> float
val neg_float : float -> float
val big_num_of_ceil : float -> Nat_big_num.num
val big_num_of_floor : float -> Nat_big_num.num
type mword = int * Nat_big_num.num
val word_equal : ('a * Nat_big_num.num) -> ('a * Nat_big_num.num) -> bool
val machine_word_inject : (int * Big_int_impl.BI.big_int) -> int * Nat_big_num.num
val word_length : ('a * 'b) -> 'a
val word_concat : (int * Big_int_impl.BI.big_int) -> (int * Nat_big_num.num) -> int * Nat_big_num.num
val word_extract : int -> int -> ('a * Big_int_impl.BI.big_int) -> int * Big_int_impl.BI.big_int
val word_update : ('a * Big_int_impl.BI.big_int) -> int -> int -> ('b * Big_int_impl.BI.big_int) -> 'a * Nat_big_num.num
val word_uminus : (int * Nat_big_num.num) -> int * Nat_big_num.num
val naturalFromWord : ('a * 'b) -> 'b
val signedIntegerFromWord : (int * Big_int_impl.BI.big_int) -> Big_int_impl.BI.big_int
val wordFromBitlist : bool list -> int * Big_int_impl.BI.big_int
val bitlistFromWord : (int * Big_int_impl.BI.big_int) -> bool list
val unsignedLess : (int * Nat_big_num.num) -> (int * Nat_big_num.num) -> bool
val unsignedLessEq : (int * Nat_big_num.num) -> (int * Nat_big_num.num) -> bool
val word_not : (int * Big_int_impl.BI.big_int) -> int * Big_int_impl.BI.big_int
val word_setBit : (int * Nat_big_num.num) -> int -> bool -> int * Nat_big_num.num
val word_getBit : ('a * Big_int_impl.BI.big_int) -> int -> bool
val word_msb : (int * Big_int_impl.BI.big_int) -> bool
val word_lsb : ('a * Big_int_impl.BI.big_int) -> bool
val word_shiftLeft : ('a * Big_int_impl.BI.big_int) -> int -> 'a * Big_int_impl.BI.big_int
val word_shiftRight : ('a * Big_int_impl.BI.big_int) -> int -> 'a * Big_int_impl.BI.big_int
val word_arithShiftRight : (int * Big_int_impl.BI.big_int) -> int -> int * Big_int_impl.BI.big_int
val word_logic : ('a -> 'b -> 'c) -> (int * 'a) -> (int * 'b) -> int * 'c
val word_and : (int * Nat_big_num.num) -> (int * Nat_big_num.num) -> int * Nat_big_num.num
val word_or : (int * Nat_big_num.num) -> (int * Nat_big_num.num) -> int * Nat_big_num.num
val word_xor : (int * Nat_big_num.num) -> (int * Nat_big_num.num) -> int * Nat_big_num.num
val word_ror : int -> (int * Big_int_impl.BI.big_int) -> int * Nat_big_num.num
val word_rol : int -> (int * Big_int_impl.BI.big_int) -> int * Nat_big_num.num
val word_bin_arith : ('a -> 'b -> Big_int_impl.BI.big_int) -> (int * 'a) -> (int * 'b) -> int * Big_int_impl.BI.big_int
val word_plus : (int * Nat_big_num.num) -> (int * Nat_big_num.num) -> int * Big_int_impl.BI.big_int
val word_minus : (int * Nat_big_num.num) -> (int * Nat_big_num.num) -> int * Big_int_impl.BI.big_int
val word_times : (int * Nat_big_num.num) -> (int * Nat_big_num.num) -> int * Big_int_impl.BI.big_int
val word_udiv : ('a * Nat_big_num.num) -> ('b * Nat_big_num.num) -> 'a * Nat_big_num.num
val word_mod : ('a * Nat_big_num.num) -> ('b * Nat_big_num.num) -> 'a * Nat_big_num.num