lem

Lem is a tool for lightweight executable mathematics
type !'a eq_class = 'a Lem_basic_classes.eq_class = {
isEqual_method : 'a -> 'a -> bool;
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 = {
compare_method : 'a -> 'a -> int;
isLess_method : 'a -> 'a -> bool;
isLessEqual_method : 'a -> 'a -> bool;
isGreater_method : 'a -> 'a -> bool;
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 = {
max_method : 'a -> 'a -> 'a;
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 = {
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 = {
numNegate_method : 'a -> 'a;
}
type !'a numAbs_class = 'a Lem_num.numAbs_class = {
abs_method : 'a -> 'a;
}
type !'a numAdd_class = 'a Lem_num.numAdd_class = {
numAdd_method : 'a -> 'a -> 'a;
}
type !'a numMinus_class = 'a Lem_num.numMinus_class = {
numMinus_method : 'a -> 'a -> 'a;
}
type !'a numMult_class = 'a Lem_num.numMult_class = {
numMult_method : 'a -> 'a -> 'a;
}
type !'a numPow_class = 'a Lem_num.numPow_class = {
numPow_method : 'a -> int -> 'a;
}
type !'a numDivision_class = 'a Lem_num.numDivision_class = {
numDivision_method : 'a -> 'a -> 'a;
}
type !'a numIntegerDivision_class = 'a Lem_num.numIntegerDivision_class = {
div_method : 'a -> 'a -> 'a;
}
type !'a numRemainder_class = 'a Lem_num.numRemainder_class = {
mod_method : 'a -> 'a -> 'a;
}
type !'a numSucc_class = 'a Lem_num.numSucc_class = {
succ_method : 'a -> 'a;
}
type !'a numPred_class = 'a Lem_num.numPred_class = {
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 = {
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 =
| 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 = {
lnot_method : 'a -> 'a;
}
type !'a wordAnd_class = 'a Lem_word.wordAnd_class = {
land_method : 'a -> 'a -> 'a;
}
type !'a wordOr_class = 'a Lem_word.wordOr_class = {
lor_method : 'a -> 'a -> 'a;
}
type !'a wordXor_class = 'a Lem_word.wordXor_class = {
lxor_method : 'a -> 'a -> 'a;
}
type !'a wordLsl_class = 'a Lem_word.wordLsl_class = {
lsl_method : 'a -> int -> 'a;
}
type !'a wordLsr_class = 'a Lem_word.wordLsr_class = {
lsr_method : 'a -> int -> 'a;
}
type !'a wordAsr_class = 'a Lem_word.wordAsr_class = {
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 = {
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
val fromJust : 'a option -> 'a
val option_map : 'a Lem_map.mapKeyType_class -> ( 'a -> 'b -> 'c option ) -> ( 'a, 'b ) Pmap.map -> ( 'a, 'c ) Pmap.map
val integerOfChar : char -> Nat_big_num.num
val integerOfStringHelper : char list -> Nat_big_num.num
val setCompare : 'b -> 'a Lem_basic_classes.ord_class -> 'a Pset.set -> 'a Pset.set -> int
val instance_Basic_classes_SetType_set_dict : 'a Lem_basic_classes.setType_class -> 'a Pset.set Lem_basic_classes.setType_class
val leastFixedPointUnbounded : 'b -> ( 'a Pset.set -> 'a Pset.set ) -> 'a Pset.set -> 'a Pset.set
val last : 'a list -> 'a
val init : 'a list -> 'a list
val foldl1 : ( 'a -> 'a -> 'a ) -> 'a list -> 'a
val foldr1 : ( 'a -> 'a -> 'a ) -> 'a list -> 'a
val findNonPure : ( 'a -> bool ) -> 'a list -> 'a
val unfoldr : ( 'a -> ('b * 'a) option ) -> 'a -> 'b list
val stringFromNatHelper : int -> char list -> char list
val stringFromNaturalHelper : Nat_big_num.num -> char list -> char list
val stringLess : 'a -> 'a -> bool
val stringLessEq : 'a -> 'a -> bool
val stringGreater : 'a -> 'a -> bool
val stringGreaterEq : 'a -> 'a -> bool
val instance_Basic_classes_Ord_string_dict : string Lem_basic_classes.ord_class
val ensure : bool -> string -> unit
val instance_Show_Show_nat_dict : int Lem_show.show_class
val instance_Show_Show_Num_natural_dict : Nat_big_num.num Lem_show.show_class
val instance_Show_Show_Num_int_dict : int Lem_show.show_class
val instance_Show_Show_Num_integer_dict : Nat_big_num.num Lem_show.show_class
val stringFromSet : 'a -> ( 'b -> string ) -> 'b Pset.set -> string
val stringFromRelation : 'a Lem_basic_classes.eq_class -> 'a Lem_basic_classes.setType_class -> ( ('a * 'a) -> string ) -> ('a * 'a) Pset.set -> string
val instance_Show_Show_set_dict : 'a Lem_show.show_class -> 'b -> 'a Pset.set Lem_show.show_class
type !'a size_class = 'a Lem_machine_word.size_class = {
size_method : int;
}
val size_itself : 'a size_class -> 'b -> int
val instance_Machine_word_Size_Machine_word_ty1_dict : ty1 size_class
val instance_Machine_word_Size_Machine_word_ty2_dict : ty2 size_class
val instance_Machine_word_Size_Machine_word_ty3_dict : ty3 size_class
val instance_Machine_word_Size_Machine_word_ty4_dict : ty4 size_class
val instance_Machine_word_Size_Machine_word_ty5_dict : ty5 size_class
val instance_Machine_word_Size_Machine_word_ty6_dict : ty6 size_class
val instance_Machine_word_Size_Machine_word_ty7_dict : ty7 size_class
val instance_Machine_word_Size_Machine_word_ty8_dict : ty8 size_class
val instance_Machine_word_Size_Machine_word_ty9_dict : ty9 size_class
val instance_Machine_word_Size_Machine_word_ty10_dict : ty10 size_class
val instance_Machine_word_Size_Machine_word_ty11_dict : ty11 size_class
val instance_Machine_word_Size_Machine_word_ty12_dict : ty12 size_class
val instance_Machine_word_Size_Machine_word_ty13_dict : ty13 size_class
val instance_Machine_word_Size_Machine_word_ty14_dict : ty14 size_class
val instance_Machine_word_Size_Machine_word_ty15_dict : ty15 size_class
val instance_Machine_word_Size_Machine_word_ty16_dict : ty16 size_class
val instance_Machine_word_Size_Machine_word_ty17_dict : ty17 size_class
val instance_Machine_word_Size_Machine_word_ty18_dict : ty18 size_class
val instance_Machine_word_Size_Machine_word_ty19_dict : ty19 size_class
val instance_Machine_word_Size_Machine_word_ty20_dict : ty20 size_class
val instance_Machine_word_Size_Machine_word_ty21_dict : ty21 size_class
val instance_Machine_word_Size_Machine_word_ty22_dict : ty22 size_class
val instance_Machine_word_Size_Machine_word_ty23_dict : ty23 size_class
val instance_Machine_word_Size_Machine_word_ty24_dict : ty24 size_class
val instance_Machine_word_Size_Machine_word_ty25_dict : ty25 size_class
val instance_Machine_word_Size_Machine_word_ty26_dict : ty26 size_class
val instance_Machine_word_Size_Machine_word_ty27_dict : ty27 size_class
val instance_Machine_word_Size_Machine_word_ty28_dict : ty28 size_class
val instance_Machine_word_Size_Machine_word_ty29_dict : ty29 size_class
val instance_Machine_word_Size_Machine_word_ty30_dict : ty30 size_class
val instance_Machine_word_Size_Machine_word_ty31_dict : ty31 size_class
val instance_Machine_word_Size_Machine_word_ty32_dict : ty32 size_class
val instance_Machine_word_Size_Machine_word_ty33_dict : ty33 size_class
val instance_Machine_word_Size_Machine_word_ty34_dict : ty34 size_class
val instance_Machine_word_Size_Machine_word_ty35_dict : ty35 size_class
val instance_Machine_word_Size_Machine_word_ty36_dict : ty36 size_class
val instance_Machine_word_Size_Machine_word_ty37_dict : ty37 size_class
val instance_Machine_word_Size_Machine_word_ty38_dict : ty38 size_class
val instance_Machine_word_Size_Machine_word_ty39_dict : ty39 size_class
val instance_Machine_word_Size_Machine_word_ty40_dict : ty40 size_class
val instance_Machine_word_Size_Machine_word_ty41_dict : ty41 size_class
val instance_Machine_word_Size_Machine_word_ty42_dict : ty42 size_class
val instance_Machine_word_Size_Machine_word_ty43_dict : ty43 size_class
val instance_Machine_word_Size_Machine_word_ty44_dict : ty44 size_class
val instance_Machine_word_Size_Machine_word_ty45_dict : ty45 size_class
val instance_Machine_word_Size_Machine_word_ty46_dict : ty46 size_class
val instance_Machine_word_Size_Machine_word_ty47_dict : ty47 size_class
val instance_Machine_word_Size_Machine_word_ty48_dict : ty48 size_class
val instance_Machine_word_Size_Machine_word_ty49_dict : ty49 size_class
val instance_Machine_word_Size_Machine_word_ty50_dict : ty50 size_class
val instance_Machine_word_Size_Machine_word_ty51_dict : ty51 size_class
val instance_Machine_word_Size_Machine_word_ty52_dict : ty52 size_class
val instance_Machine_word_Size_Machine_word_ty53_dict : ty53 size_class
val instance_Machine_word_Size_Machine_word_ty54_dict : ty54 size_class
val instance_Machine_word_Size_Machine_word_ty55_dict : ty55 size_class
val instance_Machine_word_Size_Machine_word_ty56_dict : ty56 size_class
val instance_Machine_word_Size_Machine_word_ty57_dict : ty57 size_class
val instance_Machine_word_Size_Machine_word_ty58_dict : ty58 size_class
val instance_Machine_word_Size_Machine_word_ty59_dict : ty59 size_class
val instance_Machine_word_Size_Machine_word_ty60_dict : ty60 size_class
val instance_Machine_word_Size_Machine_word_ty61_dict : ty61 size_class
val instance_Machine_word_Size_Machine_word_ty62_dict : ty62 size_class
val instance_Machine_word_Size_Machine_word_ty63_dict : ty63 size_class
val instance_Machine_word_Size_Machine_word_ty64_dict : ty64 size_class
val instance_Machine_word_Size_Machine_word_ty65_dict : ty65 size_class
val instance_Machine_word_Size_Machine_word_ty66_dict : ty66 size_class
val instance_Machine_word_Size_Machine_word_ty67_dict : ty67 size_class
val instance_Machine_word_Size_Machine_word_ty68_dict : ty68 size_class
val instance_Machine_word_Size_Machine_word_ty69_dict : ty69 size_class
val instance_Machine_word_Size_Machine_word_ty70_dict : ty70 size_class
val instance_Machine_word_Size_Machine_word_ty71_dict : ty71 size_class
val instance_Machine_word_Size_Machine_word_ty72_dict : ty72 size_class
val instance_Machine_word_Size_Machine_word_ty73_dict : ty73 size_class
val instance_Machine_word_Size_Machine_word_ty74_dict : ty74 size_class
val instance_Machine_word_Size_Machine_word_ty75_dict : ty75 size_class
val instance_Machine_word_Size_Machine_word_ty76_dict : ty76 size_class
val instance_Machine_word_Size_Machine_word_ty77_dict : ty77 size_class
val instance_Machine_word_Size_Machine_word_ty78_dict : ty78 size_class
val instance_Machine_word_Size_Machine_word_ty79_dict : ty79 size_class
val instance_Machine_word_Size_Machine_word_ty80_dict : ty80 size_class
val instance_Machine_word_Size_Machine_word_ty81_dict : ty81 size_class
val instance_Machine_word_Size_Machine_word_ty82_dict : ty82 size_class
val instance_Machine_word_Size_Machine_word_ty83_dict : ty83 size_class
val instance_Machine_word_Size_Machine_word_ty84_dict : ty84 size_class
val instance_Machine_word_Size_Machine_word_ty85_dict : ty85 size_class
val instance_Machine_word_Size_Machine_word_ty86_dict : ty86 size_class
val instance_Machine_word_Size_Machine_word_ty87_dict : ty87 size_class
val instance_Machine_word_Size_Machine_word_ty88_dict : ty88 size_class
val instance_Machine_word_Size_Machine_word_ty89_dict : ty89 size_class
val instance_Machine_word_Size_Machine_word_ty90_dict : ty90 size_class
val instance_Machine_word_Size_Machine_word_ty91_dict : ty91 size_class
val instance_Machine_word_Size_Machine_word_ty92_dict : ty92 size_class
val instance_Machine_word_Size_Machine_word_ty93_dict : ty93 size_class
val instance_Machine_word_Size_Machine_word_ty94_dict : ty94 size_class
val instance_Machine_word_Size_Machine_word_ty95_dict : ty95 size_class
val instance_Machine_word_Size_Machine_word_ty96_dict : ty96 size_class
val instance_Machine_word_Size_Machine_word_ty97_dict : ty97 size_class
val instance_Machine_word_Size_Machine_word_ty98_dict : ty98 size_class
val instance_Machine_word_Size_Machine_word_ty99_dict : ty99 size_class
val instance_Machine_word_Size_Machine_word_ty100_dict : ty100 size_class
val instance_Machine_word_Size_Machine_word_ty101_dict : ty101 size_class
val instance_Machine_word_Size_Machine_word_ty102_dict : ty102 size_class
val instance_Machine_word_Size_Machine_word_ty103_dict : ty103 size_class
val instance_Machine_word_Size_Machine_word_ty104_dict : ty104 size_class
val instance_Machine_word_Size_Machine_word_ty105_dict : ty105 size_class
val instance_Machine_word_Size_Machine_word_ty106_dict : ty106 size_class
val instance_Machine_word_Size_Machine_word_ty107_dict : ty107 size_class
val instance_Machine_word_Size_Machine_word_ty108_dict : ty108 size_class
val instance_Machine_word_Size_Machine_word_ty109_dict : ty109 size_class
val instance_Machine_word_Size_Machine_word_ty110_dict : ty110 size_class
val instance_Machine_word_Size_Machine_word_ty111_dict : ty111 size_class
val instance_Machine_word_Size_Machine_word_ty112_dict : ty112 size_class
val instance_Machine_word_Size_Machine_word_ty113_dict : ty113 size_class
val instance_Machine_word_Size_Machine_word_ty114_dict : ty114 size_class
val instance_Machine_word_Size_Machine_word_ty115_dict : ty115 size_class
val instance_Machine_word_Size_Machine_word_ty116_dict : ty116 size_class
val instance_Machine_word_Size_Machine_word_ty117_dict : ty117 size_class
val instance_Machine_word_Size_Machine_word_ty118_dict : ty118 size_class
val instance_Machine_word_Size_Machine_word_ty119_dict : ty119 size_class
val instance_Machine_word_Size_Machine_word_ty120_dict : ty120 size_class
val instance_Machine_word_Size_Machine_word_ty121_dict : ty121 size_class
val instance_Machine_word_Size_Machine_word_ty122_dict : ty122 size_class
val instance_Machine_word_Size_Machine_word_ty123_dict : ty123 size_class
val instance_Machine_word_Size_Machine_word_ty124_dict : ty124 size_class
val instance_Machine_word_Size_Machine_word_ty125_dict : ty125 size_class
val instance_Machine_word_Size_Machine_word_ty126_dict : ty126 size_class
val instance_Machine_word_Size_Machine_word_ty127_dict : ty127 size_class
val instance_Machine_word_Size_Machine_word_ty128_dict : ty128 size_class
val instance_Machine_word_Size_Machine_word_ty129_dict : ty129 size_class
val instance_Machine_word_Size_Machine_word_ty130_dict : ty130 size_class
val instance_Machine_word_Size_Machine_word_ty131_dict : ty131 size_class
val instance_Machine_word_Size_Machine_word_ty132_dict : ty132 size_class
val instance_Machine_word_Size_Machine_word_ty133_dict : ty133 size_class
val instance_Machine_word_Size_Machine_word_ty134_dict : ty134 size_class
val instance_Machine_word_Size_Machine_word_ty135_dict : ty135 size_class
val instance_Machine_word_Size_Machine_word_ty136_dict : ty136 size_class
val instance_Machine_word_Size_Machine_word_ty137_dict : ty137 size_class
val instance_Machine_word_Size_Machine_word_ty138_dict : ty138 size_class
val instance_Machine_word_Size_Machine_word_ty139_dict : ty139 size_class
val instance_Machine_word_Size_Machine_word_ty140_dict : ty140 size_class
val instance_Machine_word_Size_Machine_word_ty141_dict : ty141 size_class
val instance_Machine_word_Size_Machine_word_ty142_dict : ty142 size_class
val instance_Machine_word_Size_Machine_word_ty143_dict : ty143 size_class
val instance_Machine_word_Size_Machine_word_ty144_dict : ty144 size_class
val instance_Machine_word_Size_Machine_word_ty145_dict : ty145 size_class
val instance_Machine_word_Size_Machine_word_ty146_dict : ty146 size_class
val instance_Machine_word_Size_Machine_word_ty147_dict : ty147 size_class
val instance_Machine_word_Size_Machine_word_ty148_dict : ty148 size_class
val instance_Machine_word_Size_Machine_word_ty149_dict : ty149 size_class
val instance_Machine_word_Size_Machine_word_ty150_dict : ty150 size_class
val instance_Machine_word_Size_Machine_word_ty151_dict : ty151 size_class
val instance_Machine_word_Size_Machine_word_ty152_dict : ty152 size_class
val instance_Machine_word_Size_Machine_word_ty153_dict : ty153 size_class
val instance_Machine_word_Size_Machine_word_ty154_dict : ty154 size_class
val instance_Machine_word_Size_Machine_word_ty155_dict : ty155 size_class
val instance_Machine_word_Size_Machine_word_ty156_dict : ty156 size_class
val instance_Machine_word_Size_Machine_word_ty157_dict : ty157 size_class
val instance_Machine_word_Size_Machine_word_ty158_dict : ty158 size_class
val instance_Machine_word_Size_Machine_word_ty159_dict : ty159 size_class
val instance_Machine_word_Size_Machine_word_ty160_dict : ty160 size_class
val instance_Machine_word_Size_Machine_word_ty161_dict : ty161 size_class
val instance_Machine_word_Size_Machine_word_ty162_dict : ty162 size_class
val instance_Machine_word_Size_Machine_word_ty163_dict : ty163 size_class
val instance_Machine_word_Size_Machine_word_ty164_dict : ty164 size_class
val instance_Machine_word_Size_Machine_word_ty165_dict : ty165 size_class
val instance_Machine_word_Size_Machine_word_ty166_dict : ty166 size_class
val instance_Machine_word_Size_Machine_word_ty167_dict : ty167 size_class
val instance_Machine_word_Size_Machine_word_ty168_dict : ty168 size_class
val instance_Machine_word_Size_Machine_word_ty169_dict : ty169 size_class
val instance_Machine_word_Size_Machine_word_ty170_dict : ty170 size_class
val instance_Machine_word_Size_Machine_word_ty171_dict : ty171 size_class
val instance_Machine_word_Size_Machine_word_ty172_dict : ty172 size_class
val instance_Machine_word_Size_Machine_word_ty173_dict : ty173 size_class
val instance_Machine_word_Size_Machine_word_ty174_dict : ty174 size_class
val instance_Machine_word_Size_Machine_word_ty175_dict : ty175 size_class
val instance_Machine_word_Size_Machine_word_ty176_dict : ty176 size_class
val instance_Machine_word_Size_Machine_word_ty177_dict : ty177 size_class
val instance_Machine_word_Size_Machine_word_ty178_dict : ty178 size_class
val instance_Machine_word_Size_Machine_word_ty179_dict : ty179 size_class
val instance_Machine_word_Size_Machine_word_ty180_dict : ty180 size_class
val instance_Machine_word_Size_Machine_word_ty181_dict : ty181 size_class
val instance_Machine_word_Size_Machine_word_ty182_dict : ty182 size_class
val instance_Machine_word_Size_Machine_word_ty183_dict : ty183 size_class
val instance_Machine_word_Size_Machine_word_ty184_dict : ty184 size_class
val instance_Machine_word_Size_Machine_word_ty185_dict : ty185 size_class
val instance_Machine_word_Size_Machine_word_ty186_dict : ty186 size_class
val instance_Machine_word_Size_Machine_word_ty187_dict : ty187 size_class
val instance_Machine_word_Size_Machine_word_ty188_dict : ty188 size_class
val instance_Machine_word_Size_Machine_word_ty189_dict : ty189 size_class
val instance_Machine_word_Size_Machine_word_ty190_dict : ty190 size_class
val instance_Machine_word_Size_Machine_word_ty191_dict : ty191 size_class
val instance_Machine_word_Size_Machine_word_ty192_dict : ty192 size_class
val instance_Machine_word_Size_Machine_word_ty193_dict : ty193 size_class
val instance_Machine_word_Size_Machine_word_ty194_dict : ty194 size_class
val instance_Machine_word_Size_Machine_word_ty195_dict : ty195 size_class
val instance_Machine_word_Size_Machine_word_ty196_dict : ty196 size_class
val instance_Machine_word_Size_Machine_word_ty197_dict : ty197 size_class
val instance_Machine_word_Size_Machine_word_ty198_dict : ty198 size_class
val instance_Machine_word_Size_Machine_word_ty199_dict : ty199 size_class
val instance_Machine_word_Size_Machine_word_ty200_dict : ty200 size_class
val instance_Machine_word_Size_Machine_word_ty201_dict : ty201 size_class
val instance_Machine_word_Size_Machine_word_ty202_dict : ty202 size_class
val instance_Machine_word_Size_Machine_word_ty203_dict : ty203 size_class
val instance_Machine_word_Size_Machine_word_ty204_dict : ty204 size_class
val instance_Machine_word_Size_Machine_word_ty205_dict : ty205 size_class
val instance_Machine_word_Size_Machine_word_ty206_dict : ty206 size_class
val instance_Machine_word_Size_Machine_word_ty207_dict : ty207 size_class
val instance_Machine_word_Size_Machine_word_ty208_dict : ty208 size_class
val instance_Machine_word_Size_Machine_word_ty209_dict : ty209 size_class
val instance_Machine_word_Size_Machine_word_ty210_dict : ty210 size_class
val instance_Machine_word_Size_Machine_word_ty211_dict : ty211 size_class
val instance_Machine_word_Size_Machine_word_ty212_dict : ty212 size_class
val instance_Machine_word_Size_Machine_word_ty213_dict : ty213 size_class
val instance_Machine_word_Size_Machine_word_ty214_dict : ty214 size_class
val instance_Machine_word_Size_Machine_word_ty215_dict : ty215 size_class
val instance_Machine_word_Size_Machine_word_ty216_dict : ty216 size_class
val instance_Machine_word_Size_Machine_word_ty217_dict : ty217 size_class
val instance_Machine_word_Size_Machine_word_ty218_dict : ty218 size_class
val instance_Machine_word_Size_Machine_word_ty219_dict : ty219 size_class
val instance_Machine_word_Size_Machine_word_ty220_dict : ty220 size_class
val instance_Machine_word_Size_Machine_word_ty221_dict : ty221 size_class
val instance_Machine_word_Size_Machine_word_ty222_dict : ty222 size_class
val instance_Machine_word_Size_Machine_word_ty223_dict : ty223 size_class
val instance_Machine_word_Size_Machine_word_ty224_dict : ty224 size_class
val instance_Machine_word_Size_Machine_word_ty225_dict : ty225 size_class
val instance_Machine_word_Size_Machine_word_ty226_dict : ty226 size_class
val instance_Machine_word_Size_Machine_word_ty227_dict : ty227 size_class
val instance_Machine_word_Size_Machine_word_ty228_dict : ty228 size_class
val instance_Machine_word_Size_Machine_word_ty229_dict : ty229 size_class
val instance_Machine_word_Size_Machine_word_ty230_dict : ty230 size_class
val instance_Machine_word_Size_Machine_word_ty231_dict : ty231 size_class
val instance_Machine_word_Size_Machine_word_ty232_dict : ty232 size_class
val instance_Machine_word_Size_Machine_word_ty233_dict : ty233 size_class
val instance_Machine_word_Size_Machine_word_ty234_dict : ty234 size_class
val instance_Machine_word_Size_Machine_word_ty235_dict : ty235 size_class
val instance_Machine_word_Size_Machine_word_ty236_dict : ty236 size_class
val instance_Machine_word_Size_Machine_word_ty237_dict : ty237 size_class
val instance_Machine_word_Size_Machine_word_ty238_dict : ty238 size_class
val instance_Machine_word_Size_Machine_word_ty239_dict : ty239 size_class
val instance_Machine_word_Size_Machine_word_ty240_dict : ty240 size_class
val instance_Machine_word_Size_Machine_word_ty241_dict : ty241 size_class
val instance_Machine_word_Size_Machine_word_ty242_dict : ty242 size_class
val instance_Machine_word_Size_Machine_word_ty243_dict : ty243 size_class
val instance_Machine_word_Size_Machine_word_ty244_dict : ty244 size_class
val instance_Machine_word_Size_Machine_word_ty245_dict : ty245 size_class
val instance_Machine_word_Size_Machine_word_ty246_dict : ty246 size_class
val instance_Machine_word_Size_Machine_word_ty247_dict : ty247 size_class
val instance_Machine_word_Size_Machine_word_ty248_dict : ty248 size_class
val instance_Machine_word_Size_Machine_word_ty249_dict : ty249 size_class
val instance_Machine_word_Size_Machine_word_ty250_dict : ty250 size_class
val instance_Machine_word_Size_Machine_word_ty251_dict : ty251 size_class
val instance_Machine_word_Size_Machine_word_ty252_dict : ty252 size_class
val instance_Machine_word_Size_Machine_word_ty253_dict : ty253 size_class
val instance_Machine_word_Size_Machine_word_ty254_dict : ty254 size_class
val instance_Machine_word_Size_Machine_word_ty255_dict : ty255 size_class
val instance_Machine_word_Size_Machine_word_ty256_dict : ty256 size_class
val instance_Machine_word_Size_Machine_word_ty257_dict : ty257 size_class
val wordFromNatural : 'a size_class -> Big_int_impl.BI.big_int -> Lem.mword
val wordToHex : 'a -> string
val instance_Show_Show_Machine_word_mword_dict : Lem.mword Lem_show.show_class
val size_test_fn : 'a size_class -> 'b -> int
val instance_Basic_classes_Eq_Machine_word_mword_dict : Lem.mword Lem_basic_classes.eq_class
val signedLess : (int * Big_int_impl.BI.big_int) -> (int * Big_int_impl.BI.big_int) -> bool
val signedLessEq : (int * Big_int_impl.BI.big_int) -> (int * Big_int_impl.BI.big_int) -> bool
val zeroExtend : 'a size_class -> ('b * Big_int_impl.BI.big_int) -> Lem.mword
val signedDivide : (int * Nat_big_num.num) -> (int * Nat_big_num.num) -> Lem.mword
val wordFromInteger : 'a size_class -> Nat_big_num.num -> Lem.mword
val signExtend : 'a size_class -> (int * Big_int_impl.BI.big_int) -> Lem.mword