package lem

  1. Overview
  2. Docs
type !'a eq_class = 'a Lem_basic_classes.eq_class = {
  1. isEqual_method : 'a -> 'a -> bool;
  2. isInequal_method : 'a -> 'a -> bool;
}
val unsafe_structural_inequality : 'a -> 'a -> bool
val instance_Basic_classes_Eq_var_dict : 'a eq_class
val instance_Basic_classes_Eq_Basic_classes_ordering_dict : int eq_class
type !'a ord_class = 'a Lem_basic_classes.ord_class = {
  1. compare_method : 'a -> 'a -> int;
  2. isLess_method : 'a -> 'a -> bool;
  3. isLessEqual_method : 'a -> 'a -> bool;
  4. isGreater_method : 'a -> 'a -> bool;
  5. isGreaterEqual_method : 'a -> 'a -> bool;
}
val genericCompare : ('a -> 'a -> bool) -> ('a -> 'a -> bool) -> 'a -> 'a -> int
val ordCompare : 'a eq_class -> 'a ord_class -> 'a -> 'a -> int
type !'a ordMaxMin_class = 'a Lem_basic_classes.ordMaxMin_class = {
  1. max_method : 'a -> 'a -> 'a;
  2. min_method : 'a -> 'a -> 'a;
}
val minByLessEqual : ('a -> 'a -> bool) -> 'a -> 'a -> 'a
val maxByLessEqual : ('a -> 'a -> bool) -> 'a -> 'a -> 'a
val instance_Basic_classes_OrdMaxMin_var_dict : 'b -> 'a ordMaxMin_class
type !'a setType_class = 'a Lem_basic_classes.setType_class = {
  1. setElemCompare_method : 'a -> 'a -> int;
}
val instance_Basic_classes_SetType_var_dict : 'a setType_class
val instance_Basic_classes_Eq_bool_dict : bool eq_class
val boolCompare : bool -> bool -> int
val instance_Basic_classes_SetType_bool_dict : bool setType_class
val instance_Basic_classes_Eq_char_dict : char eq_class
val instance_Basic_classes_Eq_string_dict : string eq_class
val instance_Basic_classes_Eq_tup2_dict : 'a eq_class -> 'b eq_class -> ('a * 'b) eq_class
val pairCompare : ('a -> 'b -> int) -> ('c -> 'd -> int) -> ('a * 'c) -> ('b * 'd) -> int
val pairLess : 'a ord_class -> 'b ord_class -> ('b * 'a) -> ('b * 'a) -> bool
val pairLessEq : 'a ord_class -> 'b ord_class -> ('b * 'a) -> ('b * 'a) -> bool
val pairGreater : 'a ord_class -> 'b ord_class -> ('a * 'b) -> ('a * 'b) -> bool
val pairGreaterEq : 'a ord_class -> 'b ord_class -> ('a * 'b) -> ('a * 'b) -> bool
val instance_Basic_classes_Ord_tup2_dict : 'a ord_class -> 'b ord_class -> ('a * 'b) ord_class
val instance_Basic_classes_SetType_tup2_dict : 'a setType_class -> 'b setType_class -> ('a * 'b) setType_class
val tripleEqual : 'a eq_class -> 'b eq_class -> 'c eq_class -> ('a * 'b * 'c) -> ('a * 'b * 'c) -> bool
val instance_Basic_classes_Eq_tup3_dict : 'a eq_class -> 'b eq_class -> 'c eq_class -> ('a * 'b * 'c) eq_class
val tripleCompare : ('a -> 'b -> int) -> ('c -> 'd -> int) -> ('e -> 'f -> int) -> ('a * 'c * 'e) -> ('b * 'd * 'f) -> int
val tripleLess : 'a ord_class -> 'b ord_class -> 'c ord_class -> ('a * 'b * 'c) -> ('a * 'b * 'c) -> bool
val tripleLessEq : 'a ord_class -> 'b ord_class -> 'c ord_class -> ('a * 'b * 'c) -> ('a * 'b * 'c) -> bool
val tripleGreater : 'a ord_class -> 'b ord_class -> 'c ord_class -> ('c * 'b * 'a) -> ('c * 'b * 'a) -> bool
val tripleGreaterEq : 'a ord_class -> 'b ord_class -> 'c ord_class -> ('c * 'b * 'a) -> ('c * 'b * 'a) -> bool
val instance_Basic_classes_Ord_tup3_dict : 'a ord_class -> 'b ord_class -> 'c ord_class -> ('a * 'b * 'c) ord_class
val instance_Basic_classes_SetType_tup3_dict : 'a setType_class -> 'b setType_class -> 'c setType_class -> ('a * 'b * 'c) setType_class
val quadrupleEqual : 'a eq_class -> 'b eq_class -> 'c eq_class -> 'd eq_class -> ('a * 'b * 'c * 'd) -> ('a * 'b * 'c * 'd) -> bool
val instance_Basic_classes_Eq_tup4_dict : 'a eq_class -> 'b eq_class -> 'c eq_class -> 'd eq_class -> ('a * 'b * 'c * 'd) eq_class
val quadrupleCompare : ('a -> 'b -> int) -> ('c -> 'd -> int) -> ('e -> 'f -> int) -> ('g -> 'h -> int) -> ('a * 'c * 'e * 'g) -> ('b * 'd * 'f * 'h) -> int
val quadrupleLess : 'a ord_class -> 'b ord_class -> 'c ord_class -> 'd ord_class -> ('a * 'b * 'c * 'd) -> ('a * 'b * 'c * 'd) -> bool
val quadrupleLessEq : 'a ord_class -> 'b ord_class -> 'c ord_class -> 'd ord_class -> ('a * 'b * 'c * 'd) -> ('a * 'b * 'c * 'd) -> bool
val quadrupleGreater : 'a ord_class -> 'b ord_class -> 'c ord_class -> 'd ord_class -> ('d * 'c * 'b * 'a) -> ('d * 'c * 'b * 'a) -> bool
val quadrupleGreaterEq : 'a ord_class -> 'b ord_class -> 'c ord_class -> 'd ord_class -> ('d * 'c * 'b * 'a) -> ('d * 'c * 'b * 'a) -> bool
val instance_Basic_classes_Ord_tup4_dict : 'a ord_class -> 'b ord_class -> 'c ord_class -> 'd ord_class -> ('a * 'b * 'c * 'd) ord_class
val instance_Basic_classes_SetType_tup4_dict : 'a setType_class -> 'b setType_class -> 'c setType_class -> 'd setType_class -> ('a * 'b * 'c * 'd) setType_class
val quintupleEqual : 'a eq_class -> 'b eq_class -> 'c eq_class -> 'd eq_class -> 'e eq_class -> ('a * 'b * 'c * 'd * 'e) -> ('a * 'b * 'c * 'd * 'e) -> bool
val instance_Basic_classes_Eq_tup5_dict : 'a eq_class -> 'b eq_class -> 'c eq_class -> 'd eq_class -> 'e eq_class -> ('a * 'b * 'c * 'd * 'e) eq_class
val quintupleCompare : ('a -> 'b -> int) -> ('c -> 'd -> int) -> ('e -> 'f -> int) -> ('g -> 'h -> int) -> ('i -> 'j -> int) -> ('a * 'c * 'e * 'g * 'i) -> ('b * 'd * 'f * 'h * 'j) -> int
val quintupleLess : 'a ord_class -> 'b ord_class -> 'c ord_class -> 'd ord_class -> 'e ord_class -> ('a * 'b * 'c * 'd * 'e) -> ('a * 'b * 'c * 'd * 'e) -> bool
val quintupleLessEq : 'a ord_class -> 'b ord_class -> 'c ord_class -> 'd ord_class -> 'e ord_class -> ('a * 'b * 'c * 'd * 'e) -> ('a * 'b * 'c * 'd * 'e) -> bool
val quintupleGreater : 'a ord_class -> 'b ord_class -> 'c ord_class -> 'd ord_class -> 'e ord_class -> ('e * 'd * 'c * 'b * 'a) -> ('e * 'd * 'c * 'b * 'a) -> bool
val quintupleGreaterEq : 'a ord_class -> 'b ord_class -> 'c ord_class -> 'd ord_class -> 'e ord_class -> ('e * 'd * 'c * 'b * 'a) -> ('e * 'd * 'c * 'b * 'a) -> bool
val instance_Basic_classes_Ord_tup5_dict : 'a ord_class -> 'b ord_class -> 'c ord_class -> 'd ord_class -> 'e ord_class -> ('a * 'b * 'c * 'd * 'e) ord_class
val instance_Basic_classes_SetType_tup5_dict : 'a setType_class -> 'b setType_class -> 'c setType_class -> 'd setType_class -> 'e setType_class -> ('a * 'b * 'c * 'd * 'e) setType_class
val sextupleEqual : 'a eq_class -> 'b eq_class -> 'c eq_class -> 'd eq_class -> 'e eq_class -> 'f eq_class -> ('a * 'b * 'c * 'd * 'e * 'f) -> ('a * 'b * 'c * 'd * 'e * 'f) -> bool
val instance_Basic_classes_Eq_tup6_dict : 'a eq_class -> 'b eq_class -> 'c eq_class -> 'd eq_class -> 'e eq_class -> 'f eq_class -> ('a * 'b * 'c * 'd * 'e * 'f) eq_class
val sextupleCompare : ('a -> 'b -> int) -> ('c -> 'd -> int) -> ('e -> 'f -> int) -> ('g -> 'h -> int) -> ('i -> 'j -> int) -> ('k -> 'l -> int) -> ('a * 'c * 'e * 'g * 'i * 'k) -> ('b * 'd * 'f * 'h * 'j * 'l) -> int
val sextupleLess : 'a ord_class -> 'b ord_class -> 'c ord_class -> 'd ord_class -> 'e ord_class -> 'f ord_class -> ('a * 'b * 'c * 'd * 'e * 'f) -> ('a * 'b * 'c * 'd * 'e * 'f) -> bool
val sextupleLessEq : 'a ord_class -> 'b ord_class -> 'c ord_class -> 'd ord_class -> 'e ord_class -> 'f ord_class -> ('a * 'b * 'c * 'd * 'e * 'f) -> ('a * 'b * 'c * 'd * 'e * 'f) -> bool
val sextupleGreater : 'a ord_class -> 'b ord_class -> 'c ord_class -> 'd ord_class -> 'e ord_class -> 'f ord_class -> ('f * 'e * 'd * 'c * 'b * 'a) -> ('f * 'e * 'd * 'c * 'b * 'a) -> bool
val sextupleGreaterEq : 'a ord_class -> 'b ord_class -> 'c ord_class -> 'd ord_class -> 'e ord_class -> 'f ord_class -> ('f * 'e * 'd * 'c * 'b * 'a) -> ('f * 'e * 'd * 'c * 'b * 'a) -> bool
val instance_Basic_classes_Ord_tup6_dict : 'a ord_class -> 'b ord_class -> 'c ord_class -> 'd ord_class -> 'e ord_class -> 'f ord_class -> ('a * 'b * 'c * 'd * 'e * 'f) ord_class
val instance_Basic_classes_SetType_tup6_dict : 'a setType_class -> 'b setType_class -> 'c setType_class -> 'd setType_class -> 'e setType_class -> 'f setType_class -> ('a * 'b * 'c * 'd * 'e * 'f) setType_class
val instance_Basic_classes_Eq_Maybe_maybe_dict : 'a Lem_basic_classes.eq_class -> 'a option Lem_basic_classes.eq_class
val maybeCompare : ('a -> 'b -> int) -> 'a option -> 'b option -> int
val instance_Basic_classes_SetType_Maybe_maybe_dict : 'a Lem_basic_classes.setType_class -> 'a option Lem_basic_classes.setType_class
val instance_Basic_classes_Ord_Maybe_maybe_dict : 'a Lem_basic_classes.ord_class -> 'a option Lem_basic_classes.ord_class
val instance_Basic_classes_Eq_Either_either_dict : 'a Lem_basic_classes.eq_class -> 'b Lem_basic_classes.eq_class -> ('a, 'b) Either.either Lem_basic_classes.eq_class
val either_setElemCompare : ('a -> 'b -> int) -> ('c -> 'd -> int) -> ('a, 'c) Either.either -> ('b, 'd) Either.either -> int
val instance_Basic_classes_SetType_Either_either_dict : 'a Lem_basic_classes.setType_class -> 'b Lem_basic_classes.setType_class -> ('a, 'b) Either.either Lem_basic_classes.setType_class
val id : 'a -> 'a
val comb : ('b -> 'c) -> ('a -> 'b) -> 'a -> 'c
val flip : ('a -> 'b -> 'c) -> 'b -> 'a -> 'c
val curry : (('a * 'b) -> 'c) -> 'a -> 'b -> 'c
val uncurry : ('a -> 'b -> 'c) -> ('a * 'b) -> 'c
type !'a numNegate_class = 'a Lem_num.numNegate_class = {
  1. numNegate_method : 'a -> 'a;
}
type !'a numAbs_class = 'a Lem_num.numAbs_class = {
  1. abs_method : 'a -> 'a;
}
type !'a numAdd_class = 'a Lem_num.numAdd_class = {
  1. numAdd_method : 'a -> 'a -> 'a;
}
type !'a numMinus_class = 'a Lem_num.numMinus_class = {
  1. numMinus_method : 'a -> 'a -> 'a;
}
type !'a numMult_class = 'a Lem_num.numMult_class = {
  1. numMult_method : 'a -> 'a -> 'a;
}
type !'a numPow_class = 'a Lem_num.numPow_class = {
  1. numPow_method : 'a -> int -> 'a;
}
type !'a numDivision_class = 'a Lem_num.numDivision_class = {
  1. numDivision_method : 'a -> 'a -> 'a;
}
type !'a numIntegerDivision_class = 'a Lem_num.numIntegerDivision_class = {
  1. div_method : 'a -> 'a -> 'a;
}
type !'a numRemainder_class = 'a Lem_num.numRemainder_class = {
  1. mod_method : 'a -> 'a -> 'a;
}
type !'a numSucc_class = 'a Lem_num.numSucc_class = {
  1. succ_method : 'a -> 'a;
}
type !'a numPred_class = 'a Lem_num.numPred_class = {
  1. pred_method : 'a -> 'a;
}
val instance_Basic_classes_Eq_nat_dict : int Lem_basic_classes.eq_class
val instance_Basic_classes_Ord_nat_dict : int Lem_basic_classes.ord_class
val instance_Basic_classes_SetType_nat_dict : int Lem_basic_classes.setType_class
val instance_Num_NumAdd_nat_dict : int numAdd_class
val instance_Num_NumMinus_nat_dict : int numMinus_class
val instance_Num_NumSucc_nat_dict : int numSucc_class
val instance_Num_NumPred_nat_dict : int numPred_class
val instance_Num_NumMult_nat_dict : int numMult_class
val instance_Num_NumIntegerDivision_nat_dict : int numIntegerDivision_class
val instance_Num_NumDivision_nat_dict : int numDivision_class
val instance_Num_NumRemainder_nat_dict : int numRemainder_class
val gen_pow_aux : ('a -> 'a -> 'a) -> 'a -> 'a -> int -> 'a
val gen_pow : 'a -> ('a -> 'a -> 'a) -> 'a -> int -> 'a
val natPow : int -> int -> int
val instance_Num_NumPow_nat_dict : int numPow_class
val instance_Basic_classes_OrdMaxMin_nat_dict : int Lem_basic_classes.ordMaxMin_class
val instance_Basic_classes_Eq_Num_natural_dict : Nat_big_num.num Lem_basic_classes.eq_class
val instance_Basic_classes_Ord_Num_natural_dict : Nat_big_num.num Lem_basic_classes.ord_class
val instance_Basic_classes_SetType_Num_natural_dict : Nat_big_num.num Lem_basic_classes.setType_class
val instance_Num_NumAdd_Num_natural_dict : Nat_big_num.num numAdd_class
val instance_Num_NumMinus_Num_natural_dict : Nat_big_num.num numMinus_class
val instance_Num_NumSucc_Num_natural_dict : Nat_big_num.num numSucc_class
val instance_Num_NumPred_Num_natural_dict : Nat_big_num.num numPred_class
val instance_Num_NumMult_Num_natural_dict : Nat_big_num.num numMult_class
val instance_Num_NumPow_Num_natural_dict : Nat_big_num.num numPow_class
val instance_Num_NumIntegerDivision_Num_natural_dict : Nat_big_num.num numIntegerDivision_class
val instance_Num_NumDivision_Num_natural_dict : Nat_big_num.num numDivision_class
val instance_Num_NumRemainder_Num_natural_dict : Nat_big_num.num numRemainder_class
val instance_Basic_classes_OrdMaxMin_Num_natural_dict : Nat_big_num.num Lem_basic_classes.ordMaxMin_class
val instance_Basic_classes_Eq_Num_int_dict : int Lem_basic_classes.eq_class
val instance_Basic_classes_Ord_Num_int_dict : int Lem_basic_classes.ord_class
val instance_Basic_classes_SetType_Num_int_dict : int Lem_basic_classes.setType_class
val instance_Num_NumNegate_Num_int_dict : int numNegate_class
val instance_Num_NumAbs_Num_int_dict : int numAbs_class
val instance_Num_NumAdd_Num_int_dict : int numAdd_class
val instance_Num_NumMinus_Num_int_dict : int numMinus_class
val instance_Num_NumSucc_Num_int_dict : int numSucc_class
val instance_Num_NumPred_Num_int_dict : int numPred_class
val instance_Num_NumMult_Num_int_dict : int numMult_class
val intPow : int -> int -> int
val instance_Num_NumPow_Num_int_dict : int numPow_class
val instance_Num_NumIntegerDivision_Num_int_dict : int numIntegerDivision_class
val instance_Num_NumDivision_Num_int_dict : int numDivision_class
val instance_Num_NumRemainder_Num_int_dict : int numRemainder_class
val instance_Basic_classes_OrdMaxMin_Num_int_dict : int Lem_basic_classes.ordMaxMin_class
val instance_Basic_classes_Eq_Num_int32_dict : Int32.t Lem_basic_classes.eq_class
val instance_Basic_classes_Ord_Num_int32_dict : Int32.t Lem_basic_classes.ord_class
val instance_Basic_classes_SetType_Num_int32_dict : Int32.t Lem_basic_classes.setType_class
val instance_Num_NumNegate_Num_int32_dict : Int32.t numNegate_class
val instance_Num_NumAbs_Num_int32_dict : Int32.t numAbs_class
val instance_Num_NumAdd_Num_int32_dict : Int32.t numAdd_class
val instance_Num_NumMinus_Num_int32_dict : Int32.t numMinus_class
val instance_Num_NumSucc_Num_int32_dict : Int32.t numSucc_class
val instance_Num_NumPred_Num_int32_dict : Int32.t numPred_class
val instance_Num_NumMult_Num_int32_dict : Int32.t numMult_class
val int32Pow : Int32.t -> int -> Int32.t
val instance_Num_NumPow_Num_int32_dict : Int32.t numPow_class
val instance_Num_NumIntegerDivision_Num_int32_dict : Int32.t numIntegerDivision_class
val instance_Num_NumDivision_Num_int32_dict : Int32.t numDivision_class
val instance_Num_NumRemainder_Num_int32_dict : Int32.t numRemainder_class
val instance_Basic_classes_OrdMaxMin_Num_int32_dict : Int32.t Lem_basic_classes.ordMaxMin_class
val instance_Basic_classes_Eq_Num_int64_dict : Int64.t Lem_basic_classes.eq_class
val instance_Basic_classes_Ord_Num_int64_dict : Int64.t Lem_basic_classes.ord_class
val instance_Basic_classes_SetType_Num_int64_dict : Int64.t Lem_basic_classes.setType_class
val instance_Num_NumNegate_Num_int64_dict : Int64.t numNegate_class
val instance_Num_NumAbs_Num_int64_dict : Int64.t numAbs_class
val instance_Num_NumAdd_Num_int64_dict : Int64.t numAdd_class
val instance_Num_NumMinus_Num_int64_dict : Int64.t numMinus_class
val instance_Num_NumSucc_Num_int64_dict : Int64.t numSucc_class
val instance_Num_NumPred_Num_int64_dict : Int64.t numPred_class
val instance_Num_NumMult_Num_int64_dict : Int64.t numMult_class
val int64Pow : Int64.t -> int -> Int64.t
val instance_Num_NumPow_Num_int64_dict : Int64.t numPow_class
val instance_Num_NumIntegerDivision_Num_int64_dict : Int64.t numIntegerDivision_class
val instance_Num_NumDivision_Num_int64_dict : Int64.t numDivision_class
val instance_Num_NumRemainder_Num_int64_dict : Int64.t numRemainder_class
val instance_Basic_classes_OrdMaxMin_Num_int64_dict : Int64.t Lem_basic_classes.ordMaxMin_class
val instance_Basic_classes_Eq_Num_integer_dict : Nat_big_num.num Lem_basic_classes.eq_class
val instance_Basic_classes_Ord_Num_integer_dict : Nat_big_num.num Lem_basic_classes.ord_class
val instance_Basic_classes_SetType_Num_integer_dict : Nat_big_num.num Lem_basic_classes.setType_class
val instance_Num_NumNegate_Num_integer_dict : Nat_big_num.num numNegate_class
val instance_Num_NumAbs_Num_integer_dict : Nat_big_num.num numAbs_class
val instance_Num_NumAdd_Num_integer_dict : Nat_big_num.num numAdd_class
val instance_Num_NumMinus_Num_integer_dict : Nat_big_num.num numMinus_class
val instance_Num_NumSucc_Num_integer_dict : Nat_big_num.num numSucc_class
val instance_Num_NumPred_Num_integer_dict : Nat_big_num.num numPred_class
val instance_Num_NumMult_Num_integer_dict : Nat_big_num.num numMult_class
val instance_Num_NumPow_Num_integer_dict : Nat_big_num.num numPow_class
val instance_Num_NumIntegerDivision_Num_integer_dict : Nat_big_num.num numIntegerDivision_class
val instance_Num_NumDivision_Num_integer_dict : Nat_big_num.num numDivision_class
val instance_Num_NumRemainder_Num_integer_dict : Nat_big_num.num numRemainder_class
val instance_Basic_classes_OrdMaxMin_Num_integer_dict : Nat_big_num.num Lem_basic_classes.ordMaxMin_class
val instance_Basic_classes_Eq_Num_rational_dict : Rational.t Lem_basic_classes.eq_class
val instance_Basic_classes_Ord_Num_rational_dict : Rational.t Lem_basic_classes.ord_class
val instance_Basic_classes_SetType_Num_rational_dict : Rational.t Lem_basic_classes.setType_class
val instance_Num_NumAdd_Num_rational_dict : Rational.t numAdd_class
val instance_Num_NumMinus_Num_rational_dict : Rational.t numMinus_class
val instance_Num_NumNegate_Num_rational_dict : Rational.t numNegate_class
val instance_Num_NumAbs_Num_rational_dict : Rational.t numAbs_class
val instance_Num_NumSucc_Num_rational_dict : Rational.t numSucc_class
val instance_Num_NumPred_Num_rational_dict : Rational.t numPred_class
val instance_Num_NumMult_Num_rational_dict : Rational.t numMult_class
val instance_Num_NumDivision_Num_rational_dict : Rational.t numDivision_class
val rationalPowInteger : Rational.t -> Nat_big_num.num -> Rational.t
val rationalPowNat : Rational.t -> int -> Rational.t
val instance_Num_NumPow_Num_rational_dict : Rational.t numPow_class
val instance_Basic_classes_OrdMaxMin_Num_rational_dict : Rational.t Lem_basic_classes.ordMaxMin_class
val instance_Basic_classes_Eq_Num_real_dict : float Lem_basic_classes.eq_class
val instance_Basic_classes_Ord_Num_real_dict : float Lem_basic_classes.ord_class
val instance_Basic_classes_SetType_Num_real_dict : float Lem_basic_classes.setType_class
val instance_Num_NumAdd_Num_real_dict : float numAdd_class
val instance_Num_NumMinus_Num_real_dict : float numMinus_class
val instance_Num_NumNegate_Num_real_dict : float numNegate_class
val instance_Num_NumAbs_Num_real_dict : float numAbs_class
val instance_Num_NumSucc_Num_real_dict : float numSucc_class
val instance_Num_NumPred_Num_real_dict : float numPred_class
val instance_Num_NumMult_Num_real_dict : float numMult_class
val instance_Num_NumDivision_Num_real_dict : float numDivision_class
val realPowNat : float -> int -> float
val instance_Num_NumPow_Num_real_dict : float numPow_class
val instance_Basic_classes_OrdMaxMin_Num_real_dict : float Lem_basic_classes.ordMaxMin_class
val instance_Basic_classes_Eq_Map_map_dict : 'a -> 'v Lem_basic_classes.eq_class -> ('k, 'v) Pmap.map Lem_basic_classes.eq_class
type !'a mapKeyType_class = 'a Lem_map.mapKeyType_class = {
  1. mapKeyCompare_method : 'a -> 'a -> int;
}
val instance_Map_MapKeyType_var_dict : 'a Lem_basic_classes.setType_class -> 'a mapKeyType_class
val fromList : 'k mapKeyType_class -> ('k * 'v) list -> ('k, 'v) Pmap.map
val map_setElemCompare : 'a Lem_basic_classes.setType_class -> 'b Lem_basic_classes.setType_class -> 'c Lem_basic_classes.setType_class -> 'd Lem_basic_classes.setType_class -> 'f -> 'g -> (('d * 'c) Pset.set -> ('b * 'a) Pset.set -> 'e) -> ('d, 'c) Pmap.map -> ('b, 'a) Pmap.map -> 'e
val instance_Basic_classes_SetType_Map_map_dict : 'a Lem_basic_classes.setType_class -> 'b Lem_basic_classes.setType_class -> 'c -> ('a, 'b) Pmap.map Lem_basic_classes.setType_class
val instance_Basic_classes_Eq_set_dict : 'b -> 'a Pset.set Lem_basic_classes.eq_class
val partition : 'b -> ('a -> bool) -> 'a Pset.set -> 'a Pset.set * 'a Pset.set
val split : 'b -> 'a Lem_basic_classes.ord_class -> 'a -> 'a Pset.set -> 'a Pset.set * 'a Pset.set
val splitMember : 'b -> 'a Lem_basic_classes.ord_class -> 'a -> 'a Pset.set -> 'a Pset.set * bool * 'a Pset.set
val bigintersection : 'a Lem_basic_classes.setType_class -> 'a Pset.set Pset.set -> 'a Pset.set
val setMapMaybe : 'a -> 'b Lem_basic_classes.setType_class -> ('c -> 'b option) -> 'c Pset.set -> 'b Pset.set
val removeMaybe : 'a Lem_basic_classes.setType_class -> 'a option Pset.set -> 'a Pset.set
val leastFixedPoint : 'b -> Nat_num.nat -> ('a Pset.set -> 'a Pset.set) -> 'a Pset.set -> 'a Pset.set
val list_null : 'a list -> bool
val listEqualBy : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
val instance_Basic_classes_Eq_list_dict : 'a Lem_basic_classes.eq_class -> 'a list Lem_basic_classes.eq_class
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 instance_Basic_classes_Ord_list_dict : 'a Lem_basic_classes.ord_class -> 'a list Lem_basic_classes.ord_class
val snoc : 'a -> 'a list -> 'a list
val map_tr : 'b list -> ('a -> 'b) -> 'a list -> 'b list
val count_map : ('a -> 'b) -> 'a list -> int -> 'b list
val map : ('a -> 'b) -> 'a list -> 'b list
val dest_init_aux : 'a list -> 'a -> 'a list -> 'a list * 'a
val dest_init : 'a list -> ('a list * 'a) option
val list_index : 'a list -> Nat_num.nat -> 'a option
val find_indices_aux : int -> ('a -> bool) -> 'a list -> int list
val find_indices : ('a -> bool) -> 'a list -> int list
val find_index : ('a -> bool) -> 'a list -> int option
val genlist : (Nat_num.nat -> 'a) -> Nat_num.nat -> 'a list
val replicate : Nat_num.nat -> 'a -> 'a list
val splitAtAcc : 'a list -> Nat_num.nat -> 'a list -> 'a list * 'a list
val split_at : Nat_num.nat -> 'a list -> 'a list * 'a list
val take : Nat_num.nat -> 'a list -> 'a list
val drop : Nat_num.nat -> 'a list -> 'a list
val splitWhile_tr : ('a -> bool) -> 'a list -> 'a list -> 'a list * 'a list
val splitWhile : ('a -> bool) -> 'a list -> 'a list * 'a list
val takeWhile : ('a -> bool) -> 'a list -> 'a list
val dropWhile : ('a -> bool) -> 'a list -> 'a list
val isPrefixOf : 'a Lem_basic_classes.eq_class -> 'a list -> 'a list -> bool
val list_update : 'a list -> Nat_num.nat -> 'a -> 'a list
val elemBy : ('a -> 'b -> bool) -> 'a -> 'b list -> bool
val elem : 'a Lem_basic_classes.eq_class -> 'a -> 'a list -> bool
val list_find_opt : ('a -> bool) -> 'a list -> 'a option
val lookupBy : ('a -> 'c -> bool) -> 'a -> ('c * 'b) list -> 'b option
val reversePartition : ('a -> bool) -> 'a list -> 'a list * 'a list
val list_delete_first : ('a -> bool) -> 'a list -> 'a list option
val list_delete : ('b -> 'a -> bool) -> 'b -> 'a list -> 'a list
val list_combine : 'a list -> 'b list -> ('a * 'b) list
val instance_Basic_classes_SetType_list_dict : 'a Lem_basic_classes.setType_class -> 'a list Lem_basic_classes.setType_class
val allDistinct : 'a Lem_basic_classes.eq_class -> 'a list -> bool
val mapMaybe : ('a -> 'b option) -> 'a list -> 'b list
val mapiAux : (int -> 'b -> 'a) -> int -> 'b list -> 'a list
val mapi : (int -> 'a -> 'b) -> 'a list -> 'b list
val deletes : 'a Lem_basic_classes.eq_class -> 'a list -> 'a list -> 'a list
val catMaybes : 'a option list -> 'a list
type bitSequence = Lem_word.bitSequence =
  1. | BitSeq of int option * bool * bool list
val instance_Basic_classes_Eq_Word_bitSequence_dict : bitSequence Lem_basic_classes.eq_class
val boolListFrombitSeqAux : Nat_num.nat -> 'a -> 'a list -> 'a list
val boolListFrombitSeq : Nat_num.nat -> bitSequence -> bool list
val bitSeqFromBoolList : bool list -> bitSequence option
val cleanBitSeq : bitSequence -> bitSequence
val bitSeqTestBit : bitSequence -> Nat_num.nat -> bool option
val bitSeqSetBit : bitSequence -> Nat_num.nat -> bool -> bitSequence
val resizeBitSeq : int option -> bitSequence -> bitSequence
val bitSeqNot : bitSequence -> bitSequence
val bitSeqBinopAux : ('a -> 'b -> bool) -> 'a -> 'a list -> 'b -> 'b list -> bool list
val bitSeqBinop : (bool -> bool -> bool) -> bitSequence -> bitSequence -> bitSequence
val bitSeqAnd : bitSequence -> bitSequence -> bitSequence
val bitSeqOr : bitSequence -> bitSequence -> bitSequence
val bitSeqXor : bitSequence -> bitSequence -> bitSequence
val bitSeqShiftLeft : bitSequence -> Nat_num.nat -> bitSequence
val bitSeqArithmeticShiftRight : bitSequence -> Nat_num.nat -> bitSequence
val bitSeqLogicalShiftRight : bitSequence -> Nat_num.nat -> bitSequence
val integerFromBoolListAux : Nat_big_num.num -> bool list -> Nat_big_num.num
val integerFromBoolList : (bool * bool list) -> Nat_big_num.num
val boolListFromNatural : bool list -> Nat_big_num.num -> bool list
val boolListFromInteger : Nat_big_num.num -> bool * bool list
val bitSeqFromInteger : int option -> Nat_big_num.num -> bitSequence
val integerFromBitSeq : bitSequence -> Nat_big_num.num
val bitSeqArithUnaryOp : (Nat_big_num.num -> Nat_big_num.num) -> bitSequence -> bitSequence
val bitSeqArithBinTest : (Nat_big_num.num -> Nat_big_num.num -> 'a) -> bitSequence -> bitSequence -> 'a
val bitSeqLess : bitSequence -> bitSequence -> bool
val bitSeqLessEqual : bitSequence -> bitSequence -> bool
val bitSeqGreater : bitSequence -> bitSequence -> bool
val bitSeqGreaterEqual : bitSequence -> bitSequence -> bool
val bitSeqCompare : bitSequence -> bitSequence -> int
val instance_Basic_classes_Ord_Word_bitSequence_dict : bitSequence Lem_basic_classes.ord_class
val instance_Basic_classes_SetType_Word_bitSequence_dict : bitSequence Lem_basic_classes.setType_class
val bitSeqNegate : bitSequence -> bitSequence
val instance_Num_NumNegate_Word_bitSequence_dict : bitSequence Lem_num.numNegate_class
val bitSeqAdd : bitSequence -> bitSequence -> bitSequence
val instance_Num_NumAdd_Word_bitSequence_dict : bitSequence Lem_num.numAdd_class
val bitSeqMinus : bitSequence -> bitSequence -> bitSequence
val instance_Num_NumMinus_Word_bitSequence_dict : bitSequence Lem_num.numMinus_class
val bitSeqSucc : bitSequence -> bitSequence
val instance_Num_NumSucc_Word_bitSequence_dict : bitSequence Lem_num.numSucc_class
val bitSeqPred : bitSequence -> bitSequence
val instance_Num_NumPred_Word_bitSequence_dict : bitSequence Lem_num.numPred_class
val bitSeqMult : bitSequence -> bitSequence -> bitSequence
val instance_Num_NumMult_Word_bitSequence_dict : bitSequence Lem_num.numMult_class
val bitSeqPow : bitSequence -> int -> bitSequence
val instance_Num_NumPow_Word_bitSequence_dict : bitSequence Lem_num.numPow_class
val bitSeqDiv : bitSequence -> bitSequence -> bitSequence
val instance_Num_NumIntegerDivision_Word_bitSequence_dict : bitSequence Lem_num.numIntegerDivision_class
val instance_Num_NumDivision_Word_bitSequence_dict : bitSequence Lem_num.numDivision_class
val bitSeqMod : bitSequence -> bitSequence -> bitSequence
val instance_Num_NumRemainder_Word_bitSequence_dict : bitSequence Lem_num.numRemainder_class
val bitSeqMin : bitSequence -> bitSequence -> bitSequence
val bitSeqMax : bitSequence -> bitSequence -> bitSequence
val instance_Basic_classes_OrdMaxMin_Word_bitSequence_dict : bitSequence Lem_basic_classes.ordMaxMin_class
type !'a wordNot_class = 'a Lem_word.wordNot_class = {
  1. lnot_method : 'a -> 'a;
}
type !'a wordAnd_class = 'a Lem_word.wordAnd_class = {
  1. land_method : 'a -> 'a -> 'a;
}
type !'a wordOr_class = 'a Lem_word.wordOr_class = {
  1. lor_method : 'a -> 'a -> 'a;
}
type !'a wordXor_class = 'a Lem_word.wordXor_class = {
  1. lxor_method : 'a -> 'a -> 'a;
}
type !'a wordLsl_class = 'a Lem_word.wordLsl_class = {
  1. lsl_method : 'a -> int -> 'a;
}
type !'a wordLsr_class = 'a Lem_word.wordLsr_class = {
  1. lsr_method : 'a -> int -> 'a;
}
type !'a wordAsr_class = 'a Lem_word.wordAsr_class = {
  1. asr_method : 'a -> int -> 'a;
}
val instance_Word_WordNot_Word_bitSequence_dict : bitSequence wordNot_class
val instance_Word_WordAnd_Word_bitSequence_dict : bitSequence wordAnd_class
val instance_Word_WordOr_Word_bitSequence_dict : bitSequence wordOr_class
val instance_Word_WordXor_Word_bitSequence_dict : bitSequence wordXor_class
val instance_Word_WordLsl_Word_bitSequence_dict : bitSequence wordLsl_class
val instance_Word_WordLsr_Word_bitSequence_dict : bitSequence wordLsr_class
val instance_Word_WordAsr_Word_bitSequence_dict : bitSequence wordAsr_class
val instance_Word_WordNot_Num_int32_dict : Int32.t wordNot_class
val instance_Word_WordOr_Num_int32_dict : Int32.t wordOr_class
val instance_Word_WordXor_Num_int32_dict : Int32.t wordXor_class
val instance_Word_WordAnd_Num_int32_dict : Int32.t wordAnd_class
val instance_Word_WordLsl_Num_int32_dict : Int32.t wordLsl_class
val instance_Word_WordLsr_Num_int32_dict : Int32.t wordLsr_class
val instance_Word_WordAsr_Num_int32_dict : Int32.t wordAsr_class
val instance_Word_WordNot_Num_int64_dict : Int64.t wordNot_class
val instance_Word_WordOr_Num_int64_dict : Int64.t wordOr_class
val instance_Word_WordXor_Num_int64_dict : Int64.t wordXor_class
val instance_Word_WordAnd_Num_int64_dict : Int64.t wordAnd_class
val instance_Word_WordLsl_Num_int64_dict : Int64.t wordLsl_class
val instance_Word_WordLsr_Num_int64_dict : Int64.t wordLsr_class
val instance_Word_WordAsr_Num_int64_dict : Int64.t wordAsr_class
val defaultLnot : (bitSequence -> 'a) -> ('b -> bitSequence) -> 'b -> 'a
val defaultLand : (bitSequence -> 'a) -> ('b -> bitSequence) -> 'b -> 'b -> 'a
val defaultLor : (bitSequence -> 'a) -> ('b -> bitSequence) -> 'b -> 'b -> 'a
val defaultLxor : (bitSequence -> 'a) -> ('b -> bitSequence) -> 'b -> 'b -> 'a
val defaultLsl : (bitSequence -> 'a) -> ('b -> bitSequence) -> 'b -> Nat_num.nat -> 'a
val defaultLsr : (bitSequence -> 'a) -> ('b -> bitSequence) -> 'b -> Nat_num.nat -> 'a
val defaultAsr : (bitSequence -> 'a) -> ('b -> bitSequence) -> 'b -> Nat_num.nat -> 'a
val integerLnot : Nat_big_num.num -> Nat_big_num.num
val instance_Word_WordNot_Num_integer_dict : Nat_big_num.num wordNot_class
val instance_Word_WordOr_Num_integer_dict : Nat_big_num.num wordOr_class
val instance_Word_WordXor_Num_integer_dict : Nat_big_num.num wordXor_class
val instance_Word_WordAnd_Num_integer_dict : Nat_big_num.num wordAnd_class
val instance_Word_WordLsl_Num_integer_dict : Nat_big_num.num wordLsl_class
val instance_Word_WordLsr_Num_integer_dict : Nat_big_num.num wordLsr_class
val instance_Word_WordAsr_Num_integer_dict : Nat_big_num.num wordAsr_class
val intFromBitSeq : bitSequence -> int
val bitSeqFromInt : int -> bitSequence
val instance_Word_WordNot_Num_int_dict : int wordNot_class
val instance_Word_WordOr_Num_int_dict : int wordOr_class
val instance_Word_WordXor_Num_int_dict : int wordXor_class
val instance_Word_WordAnd_Num_int_dict : int wordAnd_class
val instance_Word_WordLsl_Num_int_dict : int wordLsl_class
val instance_Word_WordAsr_Num_int_dict : int wordAsr_class
val naturalFromBitSeq : bitSequence -> Nat_big_num.num
val bitSeqFromNatural : int option -> Nat_big_num.num -> bitSequence
val instance_Word_WordOr_Num_natural_dict : Nat_big_num.num wordOr_class
val instance_Word_WordXor_Num_natural_dict : Nat_big_num.num wordXor_class
val instance_Word_WordAnd_Num_natural_dict : Nat_big_num.num wordAnd_class
val instance_Word_WordLsl_Num_natural_dict : Nat_big_num.num wordLsl_class
val instance_Word_WordLsr_Num_natural_dict : Nat_big_num.num wordLsr_class
val instance_Word_WordAsr_Num_natural_dict : Nat_big_num.num wordAsr_class
val natFromBitSeq : bitSequence -> int
val bitSeqFromNat : int -> bitSequence
val instance_Word_WordOr_nat_dict : int wordOr_class
val instance_Word_WordXor_nat_dict : int wordXor_class
val instance_Word_WordAnd_nat_dict : int wordAnd_class
val instance_Word_WordLsl_nat_dict : int wordLsl_class
val instance_Word_WordAsr_nat_dict : int wordAsr_class
type !'a show_class = 'a Lem_show.show_class = {
  1. show_method : 'a -> string;
}
val instance_Show_Show_string_dict : string show_class
val stringFromMaybe : ('a -> string) -> 'a option -> string
val instance_Show_Show_Maybe_maybe_dict : 'a show_class -> 'a option show_class
val stringFromListAux : ('a -> string) -> 'a list -> string
val stringFromList : ('a -> string) -> 'a list -> string
val instance_Show_Show_list_dict : 'a show_class -> 'a list show_class
val stringFromPair : ('a -> string) -> ('b -> string) -> ('a * 'b) -> string
val instance_Show_Show_tup2_dict : 'a show_class -> 'b show_class -> ('a * 'b) show_class
val instance_Show_Show_bool_dict : bool show_class