structure Float32 : Type

32-bit floating-point numbers.

Float32 corresponds to the IEEE 754 binary32 format (float in C or f32 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, Float32 is special-cased by the Lean compiler to correspond to the C float type. From the point of view of Lean's logic, Float32 is equivalent to Float32.Model (via the functions Float32.toModel and Float32.ofModel), which is itself a subtype of UInt32. Some of the operations on Float32 are defined in terms of their Float32.Model counterparts, while others are opaque to Lean's kernel.

• ofModel :: (
• toModel : Model

  Converts a Float32 into a Float32.Model.

• )

def instDecidableEqFloat32.decEq (x✝ x✝¹ : Float32) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance instDecidableEqFloat32 : DecidableEq Float32

Equations

• instDecidableEqFloat32 = instDecidableEqFloat32.decEq

instance instNonemptyFloat32 : Nonempty Float32

@[extern lean_float32_add]

def Float32.add : Float32 → Float32 → Float32

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

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

Equations

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

@[extern lean_float32_sub]

def Float32.sub : Float32 → Float32 → Float32

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

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

Equations

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

@[extern lean_float32_mul]

def Float32.mul : Float32 → Float32 → Float32

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

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

Equations

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

@[extern lean_float32_div]

def Float32.div : Float32 → Float32 → Float32

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

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

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

Equations

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

@[extern lean_float32_negate]

def Float32.neg : Float32 → Float32

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

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

Equations

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

@[extern lean_float32_decLt]

def Float32.lt : Float32 → Float32 → Bool

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

Equations

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

@[extern lean_float32_decLe]

def Float32.le : Float32 → Float32 → Bool

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

Equations

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

@[extern lean_float32_of_bits]

def Float32.ofBits : UInt32 → Float32

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

Float32s and UInt32s 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 Float32.Model.

Equations

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

@[extern lean_float32_to_bits]

def Float32.toBits : Float32 → UInt32

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

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

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

Equations

• a.toBits = a.toModel.toBits

@[instance_reducible]

instance instAddFloat32 : Add Float32

Equations

• instAddFloat32 = { add := Float32.add }

@[instance_reducible]

instance instSubFloat32 : Sub Float32

Equations

• instSubFloat32 = { sub := Float32.sub }

@[instance_reducible]

instance instMulFloat32 : Mul Float32

Equations

• instMulFloat32 = { mul := Float32.mul }

@[instance_reducible]

instance instDivFloat32 : Div Float32

Equations

• instDivFloat32 = { div := Float32.div }

@[instance_reducible]

instance instNegFloat32 : Neg Float32

Equations

• instNegFloat32 = { neg := Float32.neg }

@[instance_reducible]

instance instLTFloat32 : LT Float32

Equations

• instLTFloat32 = { lt := fun (a b : Float32) => a.lt b = true }

@[instance_reducible]

instance instLEFloat32 : LE Float32

Equations

• instLEFloat32 = { le := fun (a b : Float32) => a.le b = true }

@[extern lean_float32_beq]

def Float32.beq (a b : Float32) : 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 instBEqFloat32 : BEq Float32

Equations

• instBEqFloat32 = { beq := Float32.beq }

@[instance_reducible, extern lean_float32_decLt]

instance Float32.decLt (a b : Float32) : 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_float32_decLe]

instance Float32.decLe (a b : Float32) : 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_float32_to_string]

opaque Float32.toString : Float32 → String

Converts a floating-point number to a string.

This function does not reduce in the kernel.

@[extern lean_float32_to_uint8]

def Float32.toUInt8 : Float32 → UInt8

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

If the given Float32 is non-negative, truncates the value to a positive integer, rounding down and clamping to the range of UInt8. Returns 0 if the Float32 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 Float32.Model.

Equations

• a.toUInt8 = a.toModel.toUInt8

@[extern lean_float32_to_uint16]

def Float32.toUInt16 : Float32 → UInt16

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

If the given Float32 is non-negative, truncates the value to a positive integer, rounding down and clamping to the range of UInt16. Returns 0 if the Float32 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 Float32.Model.

Equations

• a.toUInt16 = a.toModel.toUInt16

@[extern lean_float32_to_uint32]

def Float32.toUInt32 : Float32 → UInt32

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

If the given Float32 is non-negative, truncates the value to a positive integer, rounding down and clamping to the range of UInt32. Returns 0 if the Float32 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 Float32.Model.

Equations

• a.toUInt32 = a.toModel.toUInt32

@[extern lean_float32_to_uint64]

def Float32.toUInt64 : Float32 → UInt64

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

If the given Float32 is non-negative, truncates the value to a positive integer, rounding down and clamping to the range of UInt64. Returns 0 if the Float32 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 Float32.Model.

Equations

• a.toUInt64 = a.toModel.toUInt64

@[extern lean_float32_to_usize]

def Float32.toUSize : Float32 → USize

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

If the given Float32 is non-negative, truncates the value to a positive integer, rounding down and clamping to the range of USize. Returns 0 if the Float32 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 Float32.Model.

Equations

• a.toUSize = a.toModel.toUSize

@[extern lean_float32_isnan]

def Float32.isNaN : Float32 → 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 Float32.Model. It is compiled to the C operator isnan.

Equations

• a.isNaN = a.toModel.isNaN

@[extern lean_float32_isfinite]

def Float32.isFinite : Float32 → 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 Float32.Model. It is compiled to the C operator isfinite.

Equations

• a.isFinite = a.toModel.isFinite

@[extern lean_float32_isinf]

def Float32.isInf : Float32 → 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 Float32.Model. It is compiled to the C operator isinf.

Equations

• a.isInf = a.toModel.isInf

@[extern lean_float32_frexp]

opaque Float32.frExp : Float32 → Float32 × 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 instToStringFloat32 : ToString Float32

Equations

• instToStringFloat32 = { toString := Float32.toString }

@[extern lean_uint8_to_float32]

def UInt8.toFloat32 (n : UInt8) : Float32

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

Equations

• n.toFloat32 = { toModel := Float32.Model.ofUInt8 n }

@[extern lean_uint16_to_float32]

def UInt16.toFloat32 (n : UInt16) : Float32

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

Equations

• n.toFloat32 = { toModel := Float32.Model.ofUInt16 n }

@[extern lean_uint32_to_float32]

def UInt32.toFloat32 (n : UInt32) : Float32

Obtains a Float32 whose value is near the given UInt32.

It will be exactly the value of the given UInt32 if such a Float32 exists. If no such Float32 exists, the returned value will either be the smallest Float32 that is larger than the given value, or the largest Float32 that is smaller than the given value.

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

Equations

• n.toFloat32 = { toModel := Float32.Model.ofUInt32 n }

@[extern lean_uint64_to_float32]

def UInt64.toFloat32 (n : UInt64) : Float32

Obtains a Float32 whose value is near the given UInt64.

It will be exactly the value of the given UInt64 if such a Float32 exists. If no such Float32 exists, the returned value will either be the smallest Float32 that is larger than the given value, or the largest Float32 that is smaller than the given value.

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

Equations

• n.toFloat32 = { toModel := Float32.Model.ofUInt64 n }

@[extern lean_usize_to_float32]

def USize.toFloat32 (n : USize) : Float32

Obtains a Float32 whose value is near the given USize.

It will be exactly the value of the given USize if such a Float32 exists. If no such Float32 exists, the returned value will either be the smallest Float32 that is larger than the given value, or the largest Float32 that is smaller than the given value.

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

Equations

• n.toFloat32 = { toModel := Float32.Model.ofUSize n }

@[instance_reducible]

instance instInhabitedFloat32 : Inhabited Float32

Equations

• instInhabitedFloat32 = { default := UInt64.toFloat32 0 }

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

Equations

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

@[instance_reducible]

instance instReprFloat32 : Repr Float32

Equations

• instReprFloat32 = { reprPrec := Float32.repr }

@[instance_reducible]

instance instReprAtomFloat32 : ReprAtom Float32

Equations

• instReprAtomFloat32 = { }

@[extern sinf]

opaque Float32.sin : Float32 → Float32

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 sinf.

@[extern cosf]

opaque Float32.cos : Float32 → Float32

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 cosf.

@[extern tanf]

opaque Float32.tan : Float32 → Float32

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 tanf.

@[extern asinf]

opaque Float32.asin : Float32 → Float32

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 asinf.

@[extern acosf]

opaque Float32.acos : Float32 → Float32

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 acosf.

@[extern atanf]

opaque Float32.atan : Float32 → Float32

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 atanf.

@[extern atan2f]

opaque Float32.atan2 : Float32 → Float32 → Float32

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 atan2f.

@[extern sinhf]

opaque Float32.sinh : Float32 → Float32

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 sinhf.

@[extern coshf]

opaque Float32.cosh : Float32 → Float32

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 coshf.

@[extern tanhf]

opaque Float32.tanh : Float32 → Float32

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 tanhf.

@[extern asinhf]

opaque Float32.asinh : Float32 → Float32

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 asinhf.

@[extern acoshf]

opaque Float32.acosh : Float32 → Float32

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 acoshf.

@[extern atanhf]

opaque Float32.atanh : Float32 → Float32

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 atanhf.

@[extern expf]

opaque Float32.exp : Float32 → Float32

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 expf.

@[extern exp2f]

opaque Float32.exp2 : Float32 → Float32

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 exp2f.

@[extern logf]

opaque Float32.log : Float32 → Float32

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 logf.

@[extern log2f]

opaque Float32.log2 : Float32 → Float32

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 log2f.

@[extern log10f]

opaque Float32.log10 : Float32 → Float32

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 log10f.

@[extern powf]

opaque Float32.pow : Float32 → Float32 → Float32

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 powf.

@[extern sqrtf]

def Float32.sqrt : Float32 → Float32

Computes the square root of a floating-point number.

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

Equations

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

@[extern cbrtf]

opaque Float32.cbrt : Float32 → Float32

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 cbrtf.

@[extern ceilf]

opaque Float32.ceil : Float32 → Float32

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 ceilf.

Examples:

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

@[extern floorf]

opaque Float32.floor : Float32 → Float32

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 floorf.

Examples:

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

@[extern roundf]

opaque Float32.round : Float32 → Float32

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 roundf.

@[extern fabsf]

def Float32.abs : Float32 → Float32

Computes the absolute value of a floating-point number.

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

Equations

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

@[instance_reducible]

instance instHomogeneousPowFloat32 : HomogeneousPow Float32

Equations

• instHomogeneousPowFloat32 = { pow := Float32.pow }

@[instance_reducible]

instance instMinFloat32 : Min Float32

Equations

• instMinFloat32 = minOfLe

@[instance_reducible]

instance instMaxFloat32 : Max Float32

Equations

• instMaxFloat32 = maxOfLe

@[extern lean_float32_scaleb]

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

Efficiently computes x * 2^i.

This function does not reduce in the kernel.

@[extern lean_float32_to_float]

opaque Float32.toFloat : Float32 → Float

Converts a 32-bit floating-point number to a 64-bit floating-point number.

This function does not reduce in the kernel.

@[extern lean_float_to_float32]

opaque Float.toFloat32 : Float → Float32

Converts a 64-bit floating-point number to a 32-bit floating-point number. This may lose precision.

This function does not reduce in the kernel.