structure FloatSpec : Type 1

• float : Type
• val : self.float
• lt : self.float → self.float → Prop
• le : self.float → self.float → Prop
• decLt : DecidableRel self.lt
• decLe : DecidableRel self.le

opaque floatSpec : FloatSpec

structure Float : Type

Native floating point type, corresponding to the IEEE 754 binary64 format (double in C or f64 in Rust).

• val : floatSpec.float

instance instNonemptyFloat : Nonempty Float

@[extern lean_float_add]

opaque Float.add : Float → Float → Float

@[extern lean_float_sub]

opaque Float.sub : Float → Float → Float

@[extern lean_float_mul]

opaque Float.mul : Float → Float → Float

@[extern lean_float_div]

opaque Float.div : Float → Float → Float

@[extern lean_float_negate]

opaque Float.neg : Float → Float

def Float.lt : Float → Float → Prop

Equations

• a.lt b = match a, b with | { val := a }, { val := b } => floatSpec.lt a b

def Float.le : Float → Float → Prop

Equations

• a.le b = floatSpec.le a.val b.val

@[extern lean_float_of_bits]

opaque Float.ofBits : UInt64 → Float

Raw transmutation from UInt64.

Floats and UInts have the same endianness on all supported platforms. IEEE 754 very precisely specifies the bit layout of floats.

@[extern lean_float_to_bits]

opaque Float.toBits : Float → UInt64

Raw transmutation to UInt64.

Floats and UInts have the same endianness on all supported platforms. IEEE 754 very precisely specifies the bit layout of floats.

Note that this function is distinct from Float.toUInt64, which attempts to preserve the numeric value, and not the bitwise value.

instance instAddFloat : Add Float

Equations

• instAddFloat = { add := Float.add }

instance instSubFloat : Sub Float

Equations

• instSubFloat = { sub := Float.sub }

instance instMulFloat : Mul Float

Equations

• instMulFloat = { mul := Float.mul }

instance instDivFloat : Div Float

Equations

• instDivFloat = { div := Float.div }

instance instNegFloat : Neg Float

Equations

• instNegFloat = { neg := Float.neg }

instance instLTFloat : LT Float

Equations

• instLTFloat = { lt := Float.lt }

instance instLEFloat : LE Float

Equations

• instLEFloat = { le := Float.le }

@[extern lean_float_beq]

opaque Float.beq (a b : Float) : Bool

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

instance instBEqFloat : BEq Float

Equations

• instBEqFloat = { beq := Float.beq }

@[extern lean_float_decLt]

opaque Float.decLt (a b : Float) : Decidable (a < b)

@[extern lean_float_decLe]

opaque Float.decLe (a b : Float) : Decidable (a ≤ b)

instance floatDecLt (a b : Float) : Decidable (a < b)

Equations

• floatDecLt a b = a.decLt b

instance floatDecLe (a b : Float) : Decidable (a ≤ b)

Equations

• floatDecLe a b = a.decLe b

@[extern lean_float_to_string]

opaque Float.toString : Float → String

@[extern lean_float_to_uint8]

opaque Float.toUInt8 : Float → 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]

opaque Float.toUInt16 : Float → 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]

opaque Float.toUInt32 : Float → 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]

opaque Float.toUInt64 : Float → 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]

opaque Float.toUSize : Float → 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 : Float → Bool

@[extern lean_float_isfinite]

opaque Float.isFinite : Float → Bool

@[extern lean_float_isinf]

opaque Float.isInf : Float → Bool

@[extern lean_float_frexp]

opaque Float.frExp : Float → Float × Int

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.

instance instToStringFloat : ToString Float

Equations

• instToStringFloat = { toString := Float.toString }

@[extern lean_uint8_to_float]

opaque UInt8.toFloat (n : UInt8) : Float

Obtains the Float whose value is the same as the given UInt8.

@[extern lean_uint16_to_float]

opaque UInt16.toFloat (n : UInt16) : Float

Obtains the Float whose value is the same as the given UInt16.

@[extern lean_uint32_to_float]

opaque UInt32.toFloat (n : UInt32) : Float

Obtains the Float whose value is the same as the given UInt32.

@[extern lean_uint64_to_float]

opaque UInt64.toFloat (n : UInt64) : Float

Obtains a Float whose value is near the given UInt64. It will be exactly the value of the given UInt64 if such a Float exists. If no such Float exists, the returned value will either be the smallest Float this is larger than the given value, or the largest Float this is smaller than the given value.

@[extern lean_usize_to_float]

opaque USize.toFloat (n : USize) : Float

Obtains a Float whose value is near the given USize. It will be exactly the value of the given USize if such a Float exists. If no such Float exists, the returned value will either be the smallest Float this is larger than the given value, or the largest Float this is smaller than the given value.

instance instInhabitedFloat : Inhabited Float

Equations

• instInhabitedFloat = { default := UInt64.toFloat 0 }

instance instReprFloat : Repr Float

Equations

• instReprFloat = { reprPrec := fun (n : Float) (prec : Nat) => if n < UInt64.toFloat 0 then Repr.addAppParen (Std.Format.text (toString n)) prec else Std.Format.text (toString n) }

instance instReprAtomFloat : ReprAtom Float

Equations

• instReprAtomFloat = { }

@[extern sin]

opaque Float.sin : Float → Float

@[extern cos]

opaque Float.cos : Float → Float

@[extern tan]

opaque Float.tan : Float → Float

@[extern asin]

opaque Float.asin : Float → Float

@[extern acos]

opaque Float.acos : Float → Float

@[extern atan]

opaque Float.atan : Float → Float

@[extern atan2]

opaque Float.atan2 : Float → Float → Float

@[extern sinh]

opaque Float.sinh : Float → Float

@[extern cosh]

opaque Float.cosh : Float → Float

@[extern tanh]

opaque Float.tanh : Float → Float

@[extern asinh]

opaque Float.asinh : Float → Float

@[extern acosh]

opaque Float.acosh : Float → Float

@[extern atanh]

opaque Float.atanh : Float → Float

@[extern exp]

opaque Float.exp : Float → Float

@[extern exp2]

opaque Float.exp2 : Float → Float

@[extern log]

opaque Float.log : Float → Float

@[extern log2]

opaque Float.log2 : Float → Float

@[extern log10]

opaque Float.log10 : Float → Float

@[extern pow]

opaque Float.pow : Float → Float → Float

@[extern sqrt]

opaque Float.sqrt : Float → Float

@[extern cbrt]

opaque Float.cbrt : Float → Float

@[extern ceil]

opaque Float.ceil : Float → Float

@[extern floor]

opaque Float.floor : Float → Float

@[extern round]

opaque Float.round : Float → Float

@[extern fabs]

opaque Float.abs : Float → Float

instance instHomogeneousPowFloat : HomogeneousPow Float

Equations

• instHomogeneousPowFloat = { pow := Float.pow }

instance instMinFloat : Min Float

Equations

• instMinFloat = minOfLe

instance instMaxFloat : Max Float

Equations

• instMaxFloat = maxOfLe

@[extern lean_float_scaleb]

opaque Float.scaleB (x : Float) (i : Int) : Float

Efficiently computes x * 2^i.