source
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

Instances For

source
opaque floatSpec :
FloatSpec
source
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.

- val : floatSpec.float

Instances For

source
instance instNonemptyFloat :
Nonempty Float
source
@[extern lean_float_add]
opaque Float.add :
Float → Float → Float

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

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

source
@[extern lean_float_sub]
opaque Float.sub :
Float → Float → Float

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

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

source
@[extern lean_float_mul]
opaque Float.mul :
Float → Float → Float

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

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

source
@[extern lean_float_div]
opaque 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 does not reduce in the kernel. It is compiled to the C division operator.

source
@[extern lean_float_negate]
opaque Float.neg :
Float → Float

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

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

source
def Float.lt :
Float → Float → Prop

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

Equations

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

Instances For

source
def Float.le :
Float → Float → Prop

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

Equations

- a.le b = floatSpec.le a.val b.val

Instances For

source
@[extern lean_float_of_bits]
opaque 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`.

`Float`s and `UInt64`s have the same endianness on all supported platforms. IEEE 754 very precisely specifies the bit layout of floats.

This function does not reduce in the kernel.

source
@[extern lean_float_to_bits]
opaque 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`.

`Float`s and `UInt64`s 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.

source
instance instAddFloat :
Add Float
Equations

- instAddFloat = { add := Float.add }

source
instance instSubFloat :
Sub Float
Equations

- instSubFloat = { sub := Float.sub }

source
instance instMulFloat :
Mul Float
Equations

- instMulFloat = { mul := Float.mul }

source
instance instDivFloat :
Div Float
Equations

- instDivFloat = { div := Float.div }

source
instance instNegFloat :
Neg Float
Equations

- instNegFloat = { neg := Float.neg }

source
instance instLTFloat :
LT Float
Equations

- instLTFloat = { lt := Float.lt }

source
instance instLEFloat :
LE Float
Equations

- instLEFloat = { le := Float.le }

source
@[extern lean_float_beq]
opaque 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.

source
instance instBEqFloat :
BEq Float
Equations

- instBEqFloat = { beq := Float.beq }

source
@[extern lean_float_decLt]
opaque 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.

source
@[extern lean_float_decLe]
opaque 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.

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

source
@[extern lean_float_to_uint8]
opaque 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 does not reduce in the kernel.

source
@[extern lean_float_to_uint16]
opaque 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 does not reduce in the kernel.

source
@[extern lean_float_to_uint32]
opaque 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 does not reduce in the kernel.

source
@[extern lean_float_to_uint64]
opaque 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 does not reduce in the kernel.

source
@[extern lean_float_to_usize]
opaque 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 does not reduce in the kernel.

source
@[extern lean_float_isnan]
opaque 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 does not reduce in the kernel. It is compiled to the C operator `isnan`.

source
@[extern lean_float_isfinite]
opaque 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 does not reduce in the kernel. It is compiled to the C operator `isfinite`.

source
@[extern lean_float_isinf]
opaque 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 does not reduce in the kernel. It is compiled to the C operator `isinf`.

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

source
instance instToStringFloat :
ToString Float
Equations

- instToStringFloat = { toString := Float.toString }

source
@[extern lean_uint8_to_float]
opaque UInt8.toFloat (n : UInt8) :
Float

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

source
@[extern lean_uint16_to_float]
opaque UInt16.toFloat (n : UInt16) :
Float

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

source
@[extern lean_uint32_to_float]
opaque UInt32.toFloat (n : UInt32) :
Float

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

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

This function is opaque in the kernel, but is overridden at runtime with an efficient implementation.

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

This function is opaque in the kernel, but is overridden at runtime with an efficient implementation.

source
instance instInhabitedFloat :
Inhabited Float
Equations

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

source
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

Instances For

source
instance instReprFloat :
Repr Float
Equations

- instReprFloat = { reprPrec := Float.repr }

source
instance instReprAtomFloat :
ReprAtom Float
Equations

- instReprAtomFloat = { }

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

source
@[extern sqrt]
opaque Float.sqrt :
Float → Float

Computes the square root of a floating-point number.

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

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

source
@[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)`

source
@[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)`

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

source
@[extern fabs]
opaque Float.abs :
Float → Float

Computes the absolute value of a floating-point number.

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

source
instance instHomogeneousPowFloat :
HomogeneousPow Float
Equations

- instHomogeneousPowFloat = { pow := Float.pow }

source
instance instMinFloat :
Min Float
Equations

- instMinFloat = minOfLe

source
instance instMaxFloat :
Max Float
Equations

- instMaxFloat = maxOfLe

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