lem 2020-06-03 · OCaml Package

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

package lem