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, andInf
and-Inf
, which represent positive and infinities that result from dividing non-zero values by zero.
Instances For
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.
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.
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.
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.
Compares two floating point numbers for strict inequality.
This function does not reduce in the kernel. It is compiled to the C inequality operator.
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.
Converts a floating-point number to a string.
This function does not reduce in the kernel.
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.
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.
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.
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.
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.
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
.
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
.
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
.
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
.
Equations
- instToStringFloat = { toString := Float.toString }
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.
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.
Equations
- instInhabitedFloat = { default := UInt64.toFloat 0 }
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) }
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
.
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
.
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
.
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
.
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
.
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
.
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
.
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
.
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
.
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
.
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
.
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
.
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
.
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
.
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
.
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)
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)
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
.
Equations
- instHomogeneousPowFloat = { pow := Float.pow }
Efficiently computes x * 2^i
.
This function does not reduce in the kernel.