Documentation

Init.Data.Float

structure FloatSpec :
Type 1
  • float : Type
  • val : float
  • lt : floatfloatProp
  • le : floatfloatProp
  • decLt : DecidableRel lt
  • decLe : DecidableRel le
structure Float :
Type
Equations
@[extern lean_float_add]
constant Float.add :
FloatFloatFloat
@[extern lean_float_sub]
constant Float.sub :
FloatFloatFloat
@[extern lean_float_mul]
constant Float.mul :
FloatFloatFloat
@[extern lean_float_div]
constant Float.div :
FloatFloatFloat
@[extern lean_float_negate]
constant Float.neg :
noncomputable def Float.lt :
FloatFloatProp
Equations
noncomputable def Float.le :
FloatFloatProp
Equations
instance instAddFloat :
Equations
instance instSubFloat :
Equations
instance instMulFloat :
Equations
instance instDivFloat :
Equations
instance instNegFloat :
Equations
instance instLTFloat :
Equations
instance instLEFloat :
Equations
@[extern lean_float_beq]
constant Float.beq (a : Float) (b : Float) :
instance instBEqFloat :
Equations
@[extern lean_float_decLt]
constant Float.decLt (a : Float) (b : Float) :
Decidable (a < b)
@[extern lean_float_decLe]
constant Float.decLe (a : Float) (b : Float) :
instance floatDecLt (a : Float) (b : Float) :
Decidable (a < b)
Equations
instance floatDecLe (a : Float) (b : Float) :
Equations
@[extern lean_float_to_string]
constant Float.toString :
@[extern lean_float_to_uint8]
constant Float.toUInt8 :
@[extern lean_float_to_uint16]
constant Float.toUInt16 :
@[extern lean_float_to_uint32]
constant Float.toUInt32 :
@[extern lean_float_to_uint64]
constant Float.toUInt64 :
@[extern lean_float_to_usize]
constant Float.toUSize :
Equations
@[extern lean_uint64_to_float]
constant UInt64.toFloat (n : UInt64) :
@[extern sin]
constant Float.sin :
@[extern cos]
constant Float.cos :
@[extern tan]
constant Float.tan :
@[extern asin]
constant Float.asin :
@[extern acos]
constant Float.acos :
@[extern atan]
constant Float.atan :
@[extern atan2]
constant Float.atan2 :
FloatFloatFloat
@[extern sinh]
constant Float.sinh :
@[extern cosh]
constant Float.cosh :
@[extern tanh]
constant Float.tanh :
@[extern asinh]
constant Float.asinh :
@[extern acosh]
constant Float.acosh :
@[extern atanh]
constant Float.atanh :
@[extern exp]
constant Float.exp :
@[extern exp2]
constant Float.exp2 :
@[extern log]
constant Float.log :
@[extern log2]
constant Float.log2 :
@[extern log10]
constant Float.log10 :
@[extern pow]
constant Float.pow :
FloatFloatFloat
@[extern sqrt]
constant Float.sqrt :
@[extern cbrt]
constant Float.cbrt :
Equations
@[extern lean_float_scaleb]
constant Float.scaleB (x : Float) (i : Int) :

Efficiently computes x*2^i.