structure Float : Type

64-bit floating-point numbers.

Float corresponds to the IEEE 754 binary64 format (double in C or f64 in Rust). Floating-point numbers are a finite representation of a subset of the real numbers, extended with extra “sentinel” values that represent undefined and infinite results as well as separate positive and negative zeroes. Arithmetic on floating-point numbers approximates the corresponding operations on the real numbers by rounding the results to numbers that are representable, propagating error and infinite values.

Floating-point numbers include subnormal numbers. Their special values are:

• NaN, which denotes a class of “not a number” values that result from operations such as dividing zero by zero, and
• Inf and -Inf, which represent positive and infinities that result from dividing non-zero values by zero.

Like other low-level types, Float is special-cased by the Lean compiler to correspond to the C double type. From the point of view of Lean's logic, Float is equivalent to Float.Model (via the functions Float.toModel and Float.ofModel), which is itself a subtype of UInt64. Some of the operations on Float are defined in terms of their Float.Model counterparts, while others are opaque to Lean's kernel.

• ofModel :: (
• toModel : Model

  Converts a Float into a Float.Model.

• )

@[instance_reducible]

instance instDecidableEqFloat : DecidableEq Float

Equations

• instDecidableEqFloat = instDecidableEqFloat.decEq

def instDecidableEqFloat.decEq (x✝ x✝¹ : Float) : Decidable (x✝ = x✝¹)

Equations

• instDecidableEqFloat.decEq { toModel := a } { toModel := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

instance instNonemptyFloat : Nonempty Float

@[extern lean_float_add]

def Float.add : Float → Float → Float

Adds two 64-bit floating-point numbers according to IEEE 754. Typically used via the + operator.

This function has a logical model in terms of Float.Model. It is compiled to the C addition operator.

Equations

• a.add b = { toModel := a.toModel + b.toModel }

@[extern lean_float_sub]

def Float.sub : Float → Float → Float

Subtracts 64-bit floating-point numbers according to IEEE 754. Typically used via the - operator.

This function has a logical model in terms of Float.Model. It is compiled to the C subtraction operator.

Equations

• a.sub b = { toModel := a.toModel - b.toModel }

@[extern lean_float_mul]

def Float.mul : Float → Float → Float

Multiplies 64-bit floating-point numbers according to IEEE 754. Typically used via the * operator.

This function has a logical model in terms of Float.Model. It is compiled to the C multiplication operator.

Equations

• a.mul b = { toModel := a.toModel * b.toModel }

@[extern lean_float_div]

def Float.div : Float → Float → Float

Divides 64-bit floating-point numbers according to IEEE 754. Typically used via the / operator.

In Lean, division by zero typically yields zero. For Float, it instead yields either Inf, -Inf, or NaN.

This function has a logical model in terms of Float.Model. It is compiled to the C division operator.

Equations

• a.div b = { toModel := a.toModel / b.toModel }

@[extern lean_float_negate]

def Float.neg : Float → Float

Negates 64-bit floating-point numbers according to IEEE 754. Typically used via the - prefix operator.

This function has a logical model in terms of Float.Model. It is compiled to the C negation operator.

Equations

• a.neg = { toModel := -a.toModel }

@[extern lean_float_decLt]

def Float.lt : Float → Float → Bool

Strict inequality of floating-point numbers. Typically used via the < operator.

Equations

• a.lt b = decide (a.toModel < b.toModel)

@[extern lean_float_decLe]

def Float.le : Float → Float → Bool

Non-strict inequality of floating-point numbers. Typically used via the ≤ operator.

Equations

• a.le b = decide (a.toModel ≤ b.toModel)

@[extern lean_float_of_bits]

def Float.ofBits : UInt64 → Float

Bit-for-bit conversion from UInt64. Interprets a UInt64 as a Float, ignoring the numeric value and treating the UInt64's bit pattern as a Float.

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

This function has a logical model in terms of Float.Model.

Equations

• Float.ofBits a = { toModel := Float.Model.ofBits a }

@[extern lean_float_to_bits]

def Float.toBits : Float → UInt64

Bit-for-bit conversion to UInt64. Interprets a Float as a UInt64, ignoring the numeric value and treating the Float's bit pattern as a UInt64.

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

This function is distinct from Float.toUInt64, which attempts to preserve the numeric value rather than reinterpreting the bit pattern.

Equations

• a.toBits = a.toModel.toBits

@[instance_reducible]

instance instAddFloat : Add Float

Equations

• instAddFloat = { add := Float.add }

@[instance_reducible]

instance instSubFloat : Sub Float

Equations

• instSubFloat = { sub := Float.sub }

@[instance_reducible]

instance instMulFloat : Mul Float

Equations

• instMulFloat = { mul := Float.mul }

@[instance_reducible]

instance instDivFloat : Div Float

Equations

• instDivFloat = { div := Float.div }

@[instance_reducible]

instance instNegFloat : Neg Float

Equations

• instNegFloat = { neg := Float.neg }

@[instance_reducible]

instance instLTFloat : LT Float

Equations

• instLTFloat = { lt := fun (a b : Float) => a.lt b = true }

@[instance_reducible]

instance instLEFloat : LE Float

Equations

• instLEFloat = { le := fun (a b : Float) => a.le b = true }

@[extern lean_float_beq]

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

Checks whether two floating-point numbers are equal according to IEEE 754.

Floating-point equality does not correspond with propositional equality. In particular, it is not reflexive since NaN != NaN, and it is not a congruence because 0.0 == -0.0, but 1.0 / 0.0 != 1.0 / -0.0.

This function does not reduce in the kernel. It is compiled to the C equality operator.

Equations

• a.beq b = (a.toModel == b.toModel)

@[instance_reducible]

instance instBEqFloat : BEq Float

Equations

• instBEqFloat = { beq := Float.beq }

@[instance_reducible, extern lean_float_decLt]

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

Compares two floating point numbers for strict inequality.

This function does not reduce in the kernel. It is compiled to the C inequality operator.

Equations

• a.decLt b = instDecidableEqBool (a.lt b) true

@[instance_reducible, extern lean_float_decLe]

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

Compares two floating point numbers for non-strict inequality.

This function does not reduce in the kernel. It is compiled to the C inequality operator.

Equations

• a.decLe b = instDecidableEqBool (a.le b) true

@[extern lean_float_to_string]

opaque Float.toString : Float → String

Converts a floating-point number to a string.

This function does not reduce in the kernel.

@[extern lean_float_to_uint8]

def Float.toUInt8 : Float → UInt8

Converts a floating-point number to an 8-bit unsigned integer.

If the given Float is non-negative, truncates the value to a positive integer, rounding down and clamping to the range of UInt8. Returns 0 if the Float is negative or NaN, and returns the largest UInt8 value (i.e. UInt8.size - 1) if the float is larger than it.

This function has a logical model in terms of Float.Model.

Equations

• a.toUInt8 = a.toModel.toUInt8

@[extern lean_float_to_uint16]

def Float.toUInt16 : Float → UInt16

Converts a floating-point number to a 16-bit unsigned integer.

If the given Float is non-negative, truncates the value to a positive integer, rounding down and clamping to the range of UInt16. Returns 0 if the Float is negative or NaN, and returns the largest UInt16 value (i.e. UInt16.size - 1) if the float is larger than it.

This function has a logical model in terms of Float.Model.

Equations

• a.toUInt16 = a.toModel.toUInt16

@[extern lean_float_to_uint32]

def Float.toUInt32 : Float → UInt32

Converts a floating-point number to a 32-bit unsigned integer.

If the given Float is non-negative, truncates the value to a positive integer, rounding down and clamping to the range of UInt32. Returns 0 if the Float is negative or NaN, and returns the largest UInt32 value (i.e. UInt32.size - 1) if the float is larger than it.

This function has a logical model in terms of Float.Model.

Equations

• a.toUInt32 = a.toModel.toUInt32

@[extern lean_float_to_uint64]

def Float.toUInt64 : Float → UInt64

Converts a floating-point number to a 64-bit unsigned integer.

If the given Float is non-negative, truncates the value to a positive integer, rounding down and clamping to the range of UInt64. Returns 0 if the Float is negative or NaN, and returns the largest UInt64 value (i.e. UInt64.size - 1) if the float is larger than it.

This function has a logical model in terms of Float.Model.

Equations

• a.toUInt64 = a.toModel.toUInt64

@[extern lean_float_to_usize]

def Float.toUSize : Float → USize

Converts a floating-point number to a word-sized unsigned integer.

If the given Float is non-negative, truncates the value to a positive integer, rounding down and clamping to the range of USize. Returns 0 if the Float is negative or NaN, and returns the largest USize value (i.e. USize.size - 1) if the float is larger than it.

This function has a logical model in terms of Float.Model.

Equations

• a.toUSize = a.toModel.toUSize

@[extern lean_float_isnan]

def Float.isNaN : Float → Bool

Checks whether a floating point number is NaN (“not a number”) value.

NaN values result from operations that might otherwise be errors, such as dividing zero by zero.

This function has a logical model in terms of Float.Model. It is compiled to the C operator isnan.

Equations

• a.isNaN = a.toModel.isNaN

@[extern lean_float_isfinite]

def Float.isFinite : Float → Bool

Checks whether a floating-point number is finite, that is, whether it is normal, subnormal, or zero, but not infinite or NaN.

This function has a logical model in terms of Float.Model. It is compiled to the C operator isfinite.

Equations

• a.isFinite = a.toModel.isFinite

@[extern lean_float_isinf]

def Float.isInf : Float → Bool

Checks whether a floating-point number is a positive or negative infinite number, but not a finite number or NaN.

This function has a logical model in terms of Float.Model. It is compiled to the C operator isinf.

Equations

• a.isInf = a.toModel.isInf

@[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.

This function does not reduce in the kernel. It is implemented in compiled code by the C function frexp.

@[instance_reducible]

instance instToStringFloat : ToString Float

Equations

• instToStringFloat = { toString := Float.toString }

@[extern lean_uint8_to_float]

def UInt8.toFloat (n : UInt8) : Float

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

Equations

• n.toFloat = { toModel := Float.Model.ofUInt8 n }

@[extern lean_uint16_to_float]

def UInt16.toFloat (n : UInt16) : Float

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

Equations

• n.toFloat = { toModel := Float.Model.ofUInt16 n }

@[extern lean_uint32_to_float]

def UInt32.toFloat (n : UInt32) : Float

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

Equations

• n.toFloat = { toModel := Float.Model.ofUInt32 n }

@[extern lean_uint64_to_float]

def 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 that is larger than the given value, or the largest Float that is smaller than the given value.

This function has a logical model in terms of Float.Model, but is overridden at runtime with an efficient implementation.

Equations

• n.toFloat = { toModel := Float.Model.ofUInt64 n }

@[extern lean_usize_to_float]

def 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 that is larger than the given value, or the largest Float that is smaller than the given value.

This function has a logical model in terms of Float.Model, but is overridden at runtime with an efficient implementation.

Equations

• n.toFloat = { toModel := Float.Model.ofUSize n }

@[instance_reducible]

instance instInhabitedFloat : Inhabited Float

Equations

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

def Float.repr (n : Float) (prec : Nat) : Std.Format

Equations

• n.repr prec = if n < UInt64.toFloat 0 then Repr.addAppParen (Std.Format.text n.toString) prec else Std.Format.text n.toString

@[instance_reducible]

instance instReprFloat : Repr Float

Equations

• instReprFloat = { reprPrec := Float.repr }

@[instance_reducible]

instance instReprAtomFloat : ReprAtom Float

Equations

• instReprAtomFloat = { }

@[extern sin]

opaque Float.sin : Float → Float

Computes the sine of a floating-point number in radians.

This function does not reduce in the kernel. It is implemented in compiled code by the C function sin.

@[extern cos]

opaque Float.cos : Float → Float

Computes the cosine of a floating-point number in radians.

This function does not reduce in the kernel. It is implemented in compiled code by the C function cos.

@[extern tan]

opaque Float.tan : Float → Float

Computes the tangent of a floating-point number in radians.

This function does not reduce in the kernel. It is implemented in compiled code by the C function tan.

@[extern asin]

opaque Float.asin : Float → Float

Computes the arc sine (inverse sine) of a floating-point number in radians.

This function does not reduce in the kernel. It is implemented in compiled code by the C function asin.

@[extern acos]

opaque Float.acos : Float → Float

Computes the arc cosine (inverse cosine) of a floating-point number in radians.

This function does not reduce in the kernel. It is implemented in compiled code by the C function acos.

@[extern atan]

opaque Float.atan : Float → Float

Computes the arc tangent (inverse tangent) of a floating-point number in radians.

This function does not reduce in the kernel. It is implemented in compiled code by the C function atan.

@[extern atan2]

opaque Float.atan2 (y x : Float) : Float

Computes the arc tangent (inverse tangent) of y / x in radians, in the range -π–π. The signs of the arguments determine the quadrant of the result.

This function does not reduce in the kernel. It is implemented in compiled code by the C function atan2.

@[extern sinh]

opaque Float.sinh : Float → Float

Computes the hyperbolic sine of a floating-point number.

This function does not reduce in the kernel. It is implemented in compiled code by the C function sinh.

@[extern cosh]

opaque Float.cosh : Float → Float

Computes the hyperbolic cosine of a floating-point number.

This function does not reduce in the kernel. It is implemented in compiled code by the C function cosh.

@[extern tanh]

opaque Float.tanh : Float → Float

Computes the hyperbolic tangent of a floating-point number.

This function does not reduce in the kernel. It is implemented in compiled code by the C function tanh.

@[extern asinh]

opaque Float.asinh : Float → Float

Computes the hyperbolic arc sine (inverse sine) of a floating-point number.

This function does not reduce in the kernel. It is implemented in compiled code by the C function asinh.

@[extern acosh]

opaque Float.acosh : Float → Float

Computes the hyperbolic arc cosine (inverse cosine) of a floating-point number.

This function does not reduce in the kernel. It is implemented in compiled code by the C function acosh.

@[extern atanh]

opaque Float.atanh : Float → Float

Computes the hyperbolic arc tangent (inverse tangent) of a floating-point number.

This function does not reduce in the kernel. It is implemented in compiled code by the C function atanh.

@[extern exp]

opaque Float.exp (x : Float) : Float

Computes the exponential e^x of a floating-point number.

This function does not reduce in the kernel. It is implemented in compiled code by the C function exp.

@[extern exp2]

opaque Float.exp2 (x : Float) : Float

Computes the base-2 exponential 2^x of a floating-point number.

This function does not reduce in the kernel. It is implemented in compiled code by the C function exp2.

@[extern log]

opaque Float.log (x : Float) : Float

Computes the natural logarithm ln x of a floating-point number.

This function does not reduce in the kernel. It is implemented in compiled code by the C function log.

@[extern log2]

opaque Float.log2 : Float → Float

Computes the base-2 logarithm of a floating-point number.

This function does not reduce in the kernel. It is implemented in compiled code by the C function log2.

@[extern log10]

opaque Float.log10 : Float → Float

Computes the base-10 logarithm of a floating-point number.

This function does not reduce in the kernel. It is implemented in compiled code by the C function log10.

@[extern pow]

opaque Float.pow : Float → Float → Float

Raises one floating-point number to the power of another. Typically used via the ^ operator.

This function does not reduce in the kernel. It is implemented in compiled code by the C function pow.

@[extern sqrt]

def Float.sqrt : Float → Float

Computes the square root of a floating-point number.

This function has a logical model in terms of Float.Model. It is implemented in compiled code by the C function sqrt.

Equations

• a.sqrt = { toModel := a.toModel.sqrt }

@[extern cbrt]

opaque Float.cbrt : Float → Float

Computes the cube root of a floating-point number.

This function does not reduce in the kernel. It is implemented in compiled code by the C function cbrt.

@[extern ceil]

opaque Float.ceil : Float → Float

Computes the ceiling of a floating-point number, which is the smallest integer that's no smaller than the given number.

This function does not reduce in the kernel. It is implemented in compiled code by the C function ceil.

Examples:

• Float.ceil 1.5 = 2
• Float.ceil (-1.5) = (-1)

@[extern floor]

opaque Float.floor : Float → Float

Computes the floor of a floating-point number, which is the largest integer that's no larger than the given number.

This function does not reduce in the kernel. It is implemented in compiled code by the C function floor.

Examples:

• Float.floor 1.5 = 1
• Float.floor (-1.5) = (-2)

@[extern round]

opaque Float.round : Float → Float

Rounds to the nearest integer, rounding away from zero at half-way points.

This function does not reduce in the kernel. It is implemented in compiled code by the C function round.

@[extern fabs]

def Float.abs : Float → Float

Computes the absolute value of a floating-point number.

This function has a logical model in terms of Float.Model. It is implemented in compiled code by the C function fabs.

Equations

• a.abs = { toModel := a.toModel.abs }

@[instance_reducible]

instance instHomogeneousPowFloat : HomogeneousPow Float

Equations

• instHomogeneousPowFloat = { pow := Float.pow }

@[instance_reducible]

instance instMinFloat : Min Float

Equations

• instMinFloat = minOfLe

@[instance_reducible]

instance instMaxFloat : Max Float

Equations

• instMaxFloat = maxOfLe

@[extern lean_float_scaleb]

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

Efficiently computes x * 2^i.

This function does not reduce in the kernel.