Documentation

Init.Data.Float

structure FloatSpec :
Equations
@[extern lean_float_add]
opaque Float.add :
FloatFloatFloat
@[extern lean_float_sub]
opaque Float.sub :
FloatFloatFloat
@[extern lean_float_mul]
opaque Float.mul :
FloatFloatFloat
@[extern lean_float_div]
opaque Float.div :
FloatFloatFloat
@[extern lean_float_negate]
opaque Float.neg :
def Float.lt :
FloatFloatProp
Equations
  • a.lt b = match a, b with | { val := a }, { val := b } => floatSpec.lt a b
def Float.le :
FloatFloatProp
Equations
Equations
Equations
Equations
Equations
Equations
instance instLTFloat :
Equations
instance instLEFloat :
Equations
@[extern lean_float_beq]
opaque Float.beq (a : Float) (b : Float) :

Note: this is not reflexive since NaN != NaN.

Equations
@[extern lean_float_decLt]
opaque Float.decLt (a : Float) (b : Float) :
Decidable (a < b)
@[extern lean_float_decLe]
opaque 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]
@[extern lean_float_to_uint8]

If the given float is non-negative, truncates the value to the nearest non-negative integer. If negative or NaN, returns 0. If larger than the maximum value for UInt8 (including Inf), returns the maximum value of UInt8 (i.e. UInt8.size - 1).

@[extern lean_float_to_uint16]

If the given float is non-negative, truncates the value to the nearest non-negative integer. If negative or NaN, returns 0. If larger than the maximum value for UInt16 (including Inf), returns the maximum value of UInt16 (i.e. UInt16.size - 1).

@[extern lean_float_to_uint32]

If the given float is non-negative, truncates the value to the nearest non-negative integer. If negative or NaN, returns 0. If larger than the maximum value for UInt32 (including Inf), returns the maximum value of UInt32 (i.e. UInt32.size - 1).

@[extern lean_float_to_uint64]

If the given float is non-negative, truncates the value to the nearest non-negative integer. If negative or NaN, returns 0. If larger than the maximum value for UInt64 (including Inf), returns the maximum value of UInt64 (i.e. UInt64.size - 1).

@[extern lean_float_to_usize]

If the given float is non-negative, truncates the value to the nearest non-negative integer. If negative or NaN, returns 0. If larger than the maximum value for USize (including Inf), returns the maximum value of USize (i.e. USize.size - 1). This value is platform dependent).

@[extern lean_float_isnan]
opaque Float.isNaN :
@[extern lean_float_isfinite]
@[extern lean_float_isinf]
opaque Float.isInf :
@[extern lean_float_frexp]

Splits the given float x into a significand/exponent pair (s, i) such that x = s * 2^i where s ∈ (-1;-0.5] ∪ [0.5; 1). Returns an undefined value if x is not finite.

@[extern lean_uint64_to_float]
Equations
@[extern sin]
opaque Float.sin :
@[extern cos]
opaque Float.cos :
@[extern tan]
opaque Float.tan :
@[extern asin]
opaque Float.asin :
@[extern acos]
opaque Float.acos :
@[extern atan]
opaque Float.atan :
@[extern atan2]
opaque Float.atan2 :
FloatFloatFloat
@[extern sinh]
opaque Float.sinh :
@[extern cosh]
opaque Float.cosh :
@[extern tanh]
opaque Float.tanh :
@[extern asinh]
opaque Float.asinh :
@[extern acosh]
opaque Float.acosh :
@[extern atanh]
opaque Float.atanh :
@[extern exp]
opaque Float.exp :
@[extern exp2]
opaque Float.exp2 :
@[extern log]
opaque Float.log :
@[extern log2]
opaque Float.log2 :
@[extern log10]
opaque Float.log10 :
@[extern pow]
opaque Float.pow :
FloatFloatFloat
@[extern sqrt]
opaque Float.sqrt :
@[extern cbrt]
opaque Float.cbrt :
@[extern ceil]
opaque Float.ceil :
@[extern floor]
opaque Float.floor :
@[extern round]
opaque Float.round :
@[extern fabs]
opaque Float.abs :
Equations
Equations
@[extern lean_float_scaleb]
opaque Float.scaleB (x : Float) (i : Int) :

Efficiently computes x * 2^i.