lem 2022-12-10 (latest) · OCaml Package

type !'a numNegate_class = {

numNegate_method : 'a -> 'a;

}

type !'a numAbs_class = {

abs_method : 'a -> 'a;

}

type !'a numAdd_class = {

numAdd_method : 'a -> 'a -> 'a;

}

type !'a numMinus_class = {

numMinus_method : 'a -> 'a -> 'a;

}

type !'a numMult_class = {

numMult_method : 'a -> 'a -> 'a;

}

type !'a numPow_class = {

numPow_method : 'a -> int -> 'a;

}

type !'a numDivision_class = {

numDivision_method : 'a -> 'a -> 'a;

}

type !'a numIntegerDivision_class = {

div_method : 'a -> 'a -> 'a;

}

type !'a numRemainder_class = {

mod_method : 'a -> 'a -> 'a;

}

type !'a numSucc_class = {

succ_method : 'a -> 'a;

}

type !'a 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

package lem