opaque float32Spec : FloatSpec

structure Float32 : Type

Native floating point type, corresponding to the IEEE 754 binary32 format (float in C or f32 in Rust).

• val : float32Spec.float

instance instNonemptyFloat32 : Nonempty Float32

@[extern lean_float32_add]

opaque Float32.add : Float32 → Float32 → Float32

@[extern lean_float32_sub]

opaque Float32.sub : Float32 → Float32 → Float32

@[extern lean_float32_mul]

opaque Float32.mul : Float32 → Float32 → Float32

@[extern lean_float32_div]

opaque Float32.div : Float32 → Float32 → Float32

@[extern lean_float32_negate]

opaque Float32.neg : Float32 → Float32

def Float32.lt : Float32 → Float32 → Prop

Equations

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

def Float32.le : Float32 → Float32 → Prop

Equations

• a.le b = float32Spec.le a.val b.val

@[extern lean_float32_of_bits]

opaque Float32.ofBits : UInt32 → Float32

Raw transmutation from UInt32.

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

@[extern lean_float32_to_bits]

opaque Float32.toBits : Float32 → UInt32

Raw transmutation to UInt32.

Float32s 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 Float32.toUInt32, which attempts to preserve the numeric value, and not the bitwise value.

instance instAddFloat32 : Add Float32

Equations

• instAddFloat32 = { add := Float32.add }

instance instSubFloat32 : Sub Float32

Equations

• instSubFloat32 = { sub := Float32.sub }

instance instMulFloat32 : Mul Float32

Equations

• instMulFloat32 = { mul := Float32.mul }

instance instDivFloat32 : Div Float32

Equations

• instDivFloat32 = { div := Float32.div }

instance instNegFloat32 : Neg Float32

Equations

• instNegFloat32 = { neg := Float32.neg }

instance instLTFloat32 : LT Float32

Equations

• instLTFloat32 = { lt := Float32.lt }

instance instLEFloat32 : LE Float32

Equations

• instLEFloat32 = { le := Float32.le }

@[extern lean_float32_beq]

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

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

instance instBEqFloat32 : BEq Float32

Equations

• instBEqFloat32 = { beq := Float32.beq }

@[extern lean_float32_decLt]

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

@[extern lean_float32_decLe]

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

instance float32DecLt (a b : Float32) : Decidable (a < b)

Equations

• float32DecLt a b = a.decLt b

instance float32DecLe (a b : Float32) : Decidable (a ≤ b)

Equations

• float32DecLe a b = a.decLe b

@[extern lean_float32_to_string]

opaque Float32.toString : Float32 → String

@[extern lean_float32_to_uint8]

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

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

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

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

opaque Float32.toUSize : Float32 → 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_float32_isnan]

opaque Float32.isNaN : Float32 → Bool

@[extern lean_float32_isfinite]

opaque Float32.isFinite : Float32 → Bool

@[extern lean_float32_isinf]

opaque Float32.isInf : Float32 → Bool

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

instance instToStringFloat32 : ToString Float32

Equations

• instToStringFloat32 = { toString := Float32.toString }

@[extern lean_uint8_to_float32]

opaque UInt8.toFloat32 (n : UInt8) : Float32

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

@[extern lean_uint16_to_float32]

opaque UInt16.toFloat32 (n : UInt16) : Float32

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

@[extern lean_uint32_to_float32]

opaque 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 this is larger than the given value, or the largest Float32 this is smaller than the given value.

@[extern lean_uint64_to_float32]

opaque 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 this is larger than the given value, or the largest Float32 this is smaller than the given value.

@[extern lean_usize_to_float32]

opaque 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 this is larger than the given value, or the largest Float32 this is smaller than the given value.

instance instInhabitedFloat32 : Inhabited Float32

Equations

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

instance instReprFloat32 : Repr Float32

Equations

• One or more equations did not get rendered due to their size.

instance instReprAtomFloat32 : ReprAtom Float32

Equations

• instReprAtomFloat32 = { }

@[extern sinf]

opaque Float32.sin : Float32 → Float32

@[extern cosf]

opaque Float32.cos : Float32 → Float32

@[extern tanf]

opaque Float32.tan : Float32 → Float32

@[extern asinf]

opaque Float32.asin : Float32 → Float32

@[extern acosf]

opaque Float32.acos : Float32 → Float32

@[extern atanf]

opaque Float32.atan : Float32 → Float32

@[extern atan2f]

opaque Float32.atan2 : Float32 → Float32 → Float32

@[extern sinhf]

opaque Float32.sinh : Float32 → Float32

@[extern coshf]

opaque Float32.cosh : Float32 → Float32

@[extern tanhf]

opaque Float32.tanh : Float32 → Float32

@[extern asinhf]

opaque Float32.asinh : Float32 → Float32

@[extern acoshf]

opaque Float32.acosh : Float32 → Float32

@[extern atanhf]

opaque Float32.atanh : Float32 → Float32

@[extern expf]

opaque Float32.exp : Float32 → Float32

@[extern exp2f]

opaque Float32.exp2 : Float32 → Float32

@[extern logf]

opaque Float32.log : Float32 → Float32

@[extern log2f]

opaque Float32.log2 : Float32 → Float32

@[extern log10f]

opaque Float32.log10 : Float32 → Float32

@[extern powf]

opaque Float32.pow : Float32 → Float32 → Float32

@[extern sqrtf]

opaque Float32.sqrt : Float32 → Float32

@[extern cbrtf]

opaque Float32.cbrt : Float32 → Float32

@[extern ceilf]

opaque Float32.ceil : Float32 → Float32

@[extern floorf]

opaque Float32.floor : Float32 → Float32

@[extern roundf]

opaque Float32.round : Float32 → Float32

@[extern fabsf]

opaque Float32.abs : Float32 → Float32

instance instHomogeneousPowFloat32 : HomogeneousPow Float32

Equations

• instHomogeneousPowFloat32 = { pow := Float32.pow }

instance instMinFloat32 : Min Float32

Equations

• instMinFloat32 = minOfLe

instance instMaxFloat32 : Max Float32

Equations

• instMaxFloat32 = maxOfLe

@[extern lean_float32_scaleb]

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

Efficiently computes x * 2^i.

@[extern lean_float32_to_float]

opaque Float32.toFloat : Float32 → Float

@[extern lean_float_to_float32]

opaque Float.toFloat32 : Float → Float32