package lem

  1. Overview
  2. Docs
type !'a numNegate_class = {
  1. numNegate_method : 'a -> 'a;
}
type !'a numAbs_class = {
  1. abs_method : 'a -> 'a;
}
type !'a numAdd_class = {
  1. numAdd_method : 'a -> 'a -> 'a;
}
type !'a numMinus_class = {
  1. numMinus_method : 'a -> 'a -> 'a;
}
type !'a numMult_class = {
  1. numMult_method : 'a -> 'a -> 'a;
}
type !'a numPow_class = {
  1. numPow_method : 'a -> int -> 'a;
}
type !'a numDivision_class = {
  1. numDivision_method : 'a -> 'a -> 'a;
}
type !'a numIntegerDivision_class = {
  1. div_method : 'a -> 'a -> 'a;
}
type !'a numRemainder_class = {
  1. mod_method : 'a -> 'a -> 'a;
}
type !'a numSucc_class = {
  1. succ_method : 'a -> 'a;
}
type !'a 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