max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: review docstrings for Float and Float32 (#7642)

Browse source 
This PR reviews the docstrings for `Float` and `Float32`, adding missing
ones and making their format consistent.
This commit is contained in:
David Thrane Christiansen 2025-03-26 06:25:06 +01:00 • committed by GitHub
parent daa4fd9955
commit 0d1d8b6944
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
5 changed files with 791 additions and 143 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

362
src/Init/Data/Float.lean
View file

@ -26,43 +26,97 @@ opaque floatSpec : FloatSpec := {
decLe := fun _ _ => inferInstanceAs (Decidable True)
}
/-- Native floating point type, corresponding to the IEEE 754 *binary64* format
(`double` in C or `f64` in Rust). -/
/--
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](https://en.wikipedia.org/wiki/Subnormal_number).
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.
-/
structure Float where
val : floatSpec.float
instance : Nonempty Float := ⟨{ val := floatSpec.val }⟩
/--
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.
-/
@[extern "lean_float_add"] opaque Float.add : 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.
-/
@[extern "lean_float_sub"] opaque Float.sub : 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.
-/
@[extern "lean_float_mul"] opaque Float.mul : 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.
-/
@[extern "lean_float_div"] opaque Float.div : Float → 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.
-/
@[extern "lean_float_negate"] opaque Float.neg : Float → Float
set_option bootstrap.genMatcherCode false
/--
Strict inequality of floating-point numbers. Typically used via the `<` operator.
-/
def Float.lt : Float → Float → Prop := fun a b =>
match a, b with
| ⟨a⟩, ⟨b⟩ => floatSpec.lt a b
/--
Non-strict inequality of floating-point numbers. Typically used via the `≤` operator.
-/
def Float.le : Float → Float → Prop := fun a b =>
floatSpec.le a.val b.val
/--
Raw transmutation from `UInt64`.
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 UInts have the same endianness on all supported platforms.
IEEE 754 very precisely specifies the bit layout of floats.
`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.
-/
@[extern "lean_float_of_bits"] opaque Float.ofBits : UInt64 → Float
/--
Raw transmutation to `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 UInts have the same endianness on all supported platforms.
IEEE 754 very precisely specifies the bit layout of floats.
`Float`s and `UInt64`s 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 `Float.toUInt64`, which attempts
to preserve the numeric value, and not the bitwise value.
This function is distinct from `Float.toUInt64`, which attempts to preserve the numeric value rather
than reinterpreting the bit pattern.
-/
@[extern "lean_float_to_bits"] opaque Float.toBits : Float → UInt64
@ -74,15 +128,33 @@ instance : Neg Float := ⟨Float.neg⟩
instance : LT Float := ⟨Float.lt⟩
instance : LE Float := ⟨Float.le⟩
/-- Note: this is not reflexive since `NaN != NaN`.-/
/--
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.
-/
@[extern "lean_float_beq"] opaque Float.beq (a b : Float) : Bool
instance : BEq Float := ⟨Float.beq⟩
/--
Compares two floating point numbers for strict inequality.
This function does not reduce in the kernel. It is compiled to the C inequality operator.
-/
@[extern "lean_float_decLt"] opaque Float.decLt (a b : Float) : Decidable (a < b) :=
match a, b with
| ⟨a⟩, ⟨b⟩ => floatSpec.decLt 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.
-/
@[extern "lean_float_decLe"] opaque Float.decLe (a b : Float) : Decidable (a ≤ b) :=
match a, b with
| ⟨a⟩, ⟨b⟩ => floatSpec.decLe a b
@ -90,44 +162,95 @@ instance : BEq Float := ⟨Float.beq⟩
instance floatDecLt (a b : Float) : Decidable (a < b) := Float.decLt a b
instance floatDecLe (a b : Float) : Decidable (a ≤ b) := Float.decLe a b
/--
Converts a floating-point number to a string.
This function does not reduce in the kernel.
-/
@[extern "lean_float_to_string"] opaque Float.toString : Float → String
/-- 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`).
/--
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.
-/
@[extern "lean_float_to_uint8"] opaque Float.toUInt8 : Float → 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 `UInt16` (including Inf), returns the maximum value of `UInt16`
(i.e. `UInt16.size - 1`).
/--
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.
-/
@[extern "lean_float_to_uint16"] opaque Float.toUInt16 : Float → 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 `UInt32` (including Inf), returns the maximum value of `UInt32`
(i.e. `UInt32.size - 1`).
/--
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.
-/
@[extern "lean_float_to_uint32"] opaque Float.toUInt32 : Float → 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 `UInt64` (including Inf), returns the maximum value of `UInt64`
(i.e. `UInt64.size - 1`).
/--
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.
-/
@[extern "lean_float_to_uint64"] opaque Float.toUInt64 : Float → 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 `USize` (including Inf), returns the maximum value of `USize`
(i.e. `USize.size - 1`). This value is platform dependent).
/--
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.
-/
@[extern "lean_float_to_usize"] opaque Float.toUSize : Float → USize
/--
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`.
-/
@[extern "lean_float_isnan"] opaque Float.isNaN : 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`.
-/
@[extern "lean_float_isfinite"] opaque Float.isFinite : 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`.
-/
@[extern "lean_float_isinf"] opaque Float.isInf : Float → Bool
/-- 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.
/--
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`.
-/
@[extern "lean_float_frexp"] opaque Float.frExp : Float → Float × Int
@ -171,30 +294,191 @@ instance : Repr Float where
instance : ReprAtom 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 "sin"] opaque Float.sin : 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 "cos"] opaque Float.cos : 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 "tan"] opaque Float.tan : 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 "asin"] opaque Float.asin : 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 "acos"] opaque Float.acos : 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 "atan"] opaque Float.atan : Float → Float
@[extern "atan2"] opaque Float.atan2 : Float → 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 "atan2"] opaque Float.atan2 (y x : 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 "sinh"] opaque Float.sinh : 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 "cosh"] opaque Float.cosh : 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 "tanh"] opaque Float.tanh : 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 "asinh"] opaque Float.asinh : 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 "acosh"] opaque Float.acosh : 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 "atanh"] opaque Float.atanh : Float → Float
@[extern "exp"] opaque Float.exp : Float → Float
@[extern "exp2"] opaque Float.exp2 : Float → Float
@[extern "log"] opaque Float.log : 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 "exp"] opaque Float.exp (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 "exp2"] opaque Float.exp2 (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 "log"] opaque Float.log (x : 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 "log2"] opaque Float.log2 : 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 "log10"] opaque Float.log10 : 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 "pow"] opaque Float.pow : Float → 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`.
-/
@[extern "sqrt"] opaque Float.sqrt : 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 "cbrt"] opaque Float.cbrt : 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 "ceil"] opaque Float.ceil : 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 "floor"] opaque Float.floor : 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 "round"] opaque Float.round : 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`.
-/
@[extern "fabs"] opaque Float.abs : Float → Float
instance : HomogeneousPow Float := ⟨Float.pow⟩
@ -205,6 +489,8 @@ instance : Max Float := maxOfLe
/--
Efficiently computes `x * 2^i`.
This function does not reduce in the kernel.
-/
@[extern "lean_float_scaleb"]
opaque Float.scaleB (x : Float) (i : @& Int) : Float

365
src/Init/Data/Float32.lean
View file

@ -19,43 +19,101 @@ opaque float32Spec : FloatSpec := {
decLe := fun _ _ => inferInstanceAs (Decidable True)
}
/-- Native floating point type, corresponding to the IEEE 754 *binary32* format
(`float` in C or `f32` in Rust). -/
/--
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](https://en.wikipedia.org/wiki/Subnormal_number).
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.
-/
structure Float32 where
val : float32Spec.float
instance : Nonempty Float32 := ⟨{ val := float32Spec.val }⟩
/--
Adds two 32-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.
-/
@[extern "lean_float32_add"] opaque Float32.add : Float32 → Float32 → Float32
/--
Subtracts 32-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.
-/
@[extern "lean_float32_sub"] opaque Float32.sub : Float32 → Float32 → Float32
/--
Multiplies 32-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.
-/
@[extern "lean_float32_mul"] opaque Float32.mul : 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 does not reduce in the kernel. It is compiled to the C division operator.
-/
@[extern "lean_float32_div"] opaque Float32.div : Float32 → Float32 → Float32
/--
Negates 32-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.
-/
@[extern "lean_float32_negate"] opaque Float32.neg : Float32 → Float32
set_option bootstrap.genMatcherCode false
/--
Strict inequality of floating-point numbers. Typically used via the `<` operator.
-/
def Float32.lt : Float32 → Float32 → Prop := fun a b =>
match a, b with
| ⟨a⟩, ⟨b⟩ => float32Spec.lt a b
/--
Non-strict inequality of floating-point numbers. Typically used via the `≤` operator.
-/
def Float32.le : Float32 → Float32 → Prop := fun a b =>
float32Spec.le a.val b.val
/--
Raw transmutation from `UInt32`.
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 UInts have the same endianness on all supported platforms.
IEEE 754 very precisely specifies the bit layout of floats.
`Float32`s and `UInt32`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.
-/
@[extern "lean_float32_of_bits"] opaque Float32.ofBits : UInt32 → Float32
/--
Raw transmutation to `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 UInts have the same endianness on all supported platforms.
IEEE 754 very precisely specifies the bit layout of floats.
`Float32`s and `UInt32`s 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.
This function is distinct from `Float.toUInt32`, which attempts to preserve the numeric value rather
than reinterpreting the bit pattern.
This function does not reduce in the kernel.
-/
@[extern "lean_float32_to_bits"] opaque Float32.toBits : Float32 → UInt32
@ -67,15 +125,33 @@ instance : Neg Float32 := ⟨Float32.neg⟩
instance : LT Float32 := ⟨Float32.lt⟩
instance : LE Float32 := ⟨Float32.le⟩
/-- Note: this is not reflexive since `NaN != NaN`.-/
/--
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.
-/
@[extern "lean_float32_beq"] opaque Float32.beq (a b : Float32) : Bool
instance : BEq Float32 := ⟨Float32.beq⟩
/--
Compares two floating point numbers for strict inequality.
This function does not reduce in the kernel. It is compiled to the C inequality operator.
-/
@[extern "lean_float32_decLt"] opaque Float32.decLt (a b : Float32) : Decidable (a < b) :=
match a, b with
| ⟨a⟩, ⟨b⟩ => float32Spec.decLt 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.
-/
@[extern "lean_float32_decLe"] opaque Float32.decLe (a b : Float32) : Decidable (a ≤ b) :=
match a, b with
| ⟨a⟩, ⟨b⟩ => float32Spec.decLe a b
@ -83,44 +159,91 @@ instance : BEq Float32 := ⟨Float32.beq⟩
instance float32DecLt (a b : Float32) : Decidable (a < b) := Float32.decLt a b
instance float32DecLe (a b : Float32) : Decidable (a ≤ b) := Float32.decLe a b
/--
Converts a floating-point number to a string.
This function does not reduce in the kernel.
-/
@[extern "lean_float32_to_string"] opaque Float32.toString : Float32 → String
/-- 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`).
/--
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 does not reduce in the kernel.
-/
@[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 `UInt16` (including Inf), returns the maximum value of `UInt16`
(i.e. `UInt16.size - 1`).
/--
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 does not reduce in the kernel.
-/
@[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 `UInt32` (including Inf), returns the maximum value of `UInt32`
(i.e. `UInt32.size - 1`).
/--
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 does not reduce in the kernel.
-/
@[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 `UInt64` (including Inf), returns the maximum value of `UInt64`
(i.e. `UInt64.size - 1`).
/--
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 does not reduce in the kernel.
-/
@[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 `USize` (including Inf), returns the maximum value of `USize`
(i.e. `USize.size - 1`). This value is platform dependent).
/--
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 does not reduce in the kernel.
-/
@[extern "lean_float32_to_usize"] opaque Float32.toUSize : Float32 → USize
/--
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`.
-/
@[extern "lean_float32_isnan"] opaque Float32.isNaN : 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 does not reduce in the kernel. It is compiled to the C operator `isfinite`.
-/
@[extern "lean_float32_isfinite"] opaque Float32.isFinite : Float32 → 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`.
-/
@[extern "lean_float32_isinf"] opaque Float32.isInf : Float32 → Bool
/-- 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.
/--
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`.
-/
@[extern "lean_float32_frexp"] opaque Float32.frExp : Float32 → Float32 × Int
@ -172,30 +295,191 @@ instance : Repr Float32 where
instance : ReprAtom 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 "sinf"] opaque Float32.sin : 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 "cosf"] opaque Float32.cos : 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 "tanf"] opaque Float32.tan : 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 "asinf"] opaque Float32.asin : 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 "acosf"] opaque Float32.acos : 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 "atanf"] opaque Float32.atan : 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 "atan2f"] opaque Float32.atan2 : Float32 → 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 "sinhf"] opaque Float32.sinh : 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 "coshf"] opaque Float32.cosh : 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 "tanhf"] opaque Float32.tanh : 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 "asinhf"] opaque Float32.asinh : 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 "acoshf"] opaque Float32.acosh : 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 "atanhf"] opaque Float32.atanh : 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 "expf"] opaque Float32.exp : 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 "exp2f"] opaque Float32.exp2 : 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 "logf"] opaque Float32.log : 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 "log2f"] opaque Float32.log2 : 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 "log10f"] opaque Float32.log10 : 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 "powf"] opaque Float32.pow : Float32 → Float32 → Float32
/--
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
`sqrtf`.
-/
@[extern "sqrtf"] opaque Float32.sqrt : 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 "cbrtf"] opaque Float32.cbrt : 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 "ceilf"] opaque Float32.ceil : 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 "floorf"] opaque Float32.floor : 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 "roundf"] opaque Float32.round : Float32 → Float32
/--
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
`fabsf`.
-/
@[extern "fabsf"] opaque Float32.abs : Float32 → Float32
instance : HomogeneousPow Float32 := ⟨Float32.pow⟩
@ -206,9 +490,22 @@ instance : Max Float32 := maxOfLe
/--
Efficiently computes `x * 2^i`.
This function does not reduce in the kernel.
-/
@[extern "lean_float32_scaleb"]
opaque Float32.scaleB (x : Float32) (i : @& Int) : Float32
/--
Converts a 32-bit floating-point number to a 64-bit floating-point number.
This function does not reduce in the kernel.
-/
@[extern "lean_float32_to_float"] opaque Float32.toFloat : Float32 → Float
/--
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.
-/
@[extern "lean_float_to_float32"] opaque Float.toFloat32 : Float → Float32

26
src/Init/Data/OfScientific.lean
View file

@ -36,6 +36,12 @@ def Float.ofBinaryScientific (m : Nat) (e : Int) : Float :=
let e := e + s
m.toFloat.scaleB e
/--
Constructs a `Float` from the given mantissa, sign, and exponent values.
This function is part of the implementation of the `OfScientific Float` instance that is used to
interpret floating-point literals.
-/
protected opaque Float.ofScientific (m : Nat) (s : Bool) (e : Nat) : Float :=
if s then
let s := 64 - m.log2 -- ensure we have 64 bits of mantissa left after division
@ -56,12 +62,17 @@ instance : OfScientific Float where
ofScientific := Float.ofScientific
/--
Converts a natural number into a 64-bit floating point number.
Converts a natural number into the closest-possible 64-bit floating-point number, or an infinite
floating-point value if the range of `Float` is exceeded.
-/
@[export lean_float_of_nat]
def Float.ofNat (n : Nat) : Float :=
OfScientific.ofScientific n false 0
/--
Converts an integer into the closest-possible 64-bit floating-point number, or positive or negative
infinite floating-point value if the range of `Float` is exceeded.
-/
def Float.ofInt : Int → Float
| Int.ofNat n => Float.ofNat n
| Int.negSucc n => Float.neg (Float.ofNat (Nat.succ n))
@ -78,6 +89,12 @@ def Float32.ofBinaryScientific (m : Nat) (e : Int) : Float32 :=
let e := e + s
m.toFloat32.scaleB e
/--
Constructs a `Float32` from the given mantissa, sign, and exponent values.
This function is part of the implementation of the `OfScientific Float32` instance that is used to
interpret floating-point literals.
-/
protected opaque Float32.ofScientific (m : Nat) (s : Bool) (e : Nat) : Float32 :=
if s then
let s := 64 - m.log2 -- ensure we have 64 bits of mantissa left after division
@ -90,12 +107,17 @@ instance : OfScientific Float32 where
ofScientific := Float32.ofScientific
/--
Converts a natural number into a 32-bit floating point number.
Converts a natural number into the closest-possible 32-bit floating-point number, or an infinite
floating-point value if the range of `Float32` is exceeded.
-/
@[export lean_float32_of_nat]
def Float32.ofNat (n : Nat) : Float32 :=
OfScientific.ofScientific n false 0
/--
Converts an integer into the closest-possible 32-bit floating-point number, or positive or negative
infinite floating-point value if the range of `Float32` is exceeded.
-/
def Float32.ofInt : Int → Float32
| Int.ofNat n => Float32.ofNat n
| Int.negSucc n => Float32.neg (Float32.ofNat (Nat.succ n))

94
src/Init/Data/SInt/Float.lean
View file

@ -10,56 +10,77 @@ import Init.Data.SInt.Basic
set_option linter.missingDocs true
/--
Truncates the value to the nearest integer, rounding towards zero.
If NaN, returns `0`.
If larger than the maximum value for `Int8` (including Inf), returns the maximum value of `Int8`
(i.e. `Int8.maxValue`).
If smaller than the minimum value for `Int8` (including -Inf), returns the minimum value of `Int8`
(i.e. `Int8.minValue`).
Truncates a floating-point number to the nearest 8-bit signed integer, rounding towards zero.
If the `Float` is larger than the maximum value for `Int8` (including `Inf`), returns the maximum value of
`Int8` (i.e. `Int8.maxValue`). If it is smaller than the minimum value for `Int8` (including `-Inf`),
returns the minimum value of `Int8` (i.e. `Int8.minValue`). If it is `NaN`, returns `0`.
This function does not reduce in the kernel.
-/
@[extern "lean_float_to_int8"] opaque Float.toInt8 : Float → Int8
/--
Truncates the value to the nearest integer, rounding towards zero.
If NaN, returns `0`.
If larger than the maximum value for `Int16` (including Inf), returns the maximum value of `Int16`
(i.e. `Int16.maxValue`).
If smaller than the minimum value for `Int16` (including -Inf), returns the minimum value of `Int16`
(i.e. `Int16.minValue`).
Truncates a floating-point number to the nearest 16-bit signed integer, rounding towards zero.
If the `Float` is larger than the maximum value for `Int16` (including `Inf`), returns the maximum
value of `Int16` (i.e. `Int16.maxValue`). If it is smaller than the minimum value for `Int16`
(including `-Inf`), returns the minimum value of `Int16` (i.e. `Int16.minValue`). If it is `NaN`,
returns `0`.
This function does not reduce in the kernel.
-/
@[extern "lean_float_to_int16"] opaque Float.toInt16 : Float → Int16
/--
Truncates the value to the nearest integer, rounding towards zero.
If NaN, returns `0`.
If larger than the maximum value for `Int32` (including Inf), returns the maximum value of `Int32`
(i.e. `Int32.maxValue`).
If smaller than the minimum value for `Int32` (including -Inf), returns the minimum value of `Int32`
(i.e. `Int32.minValue`).
Truncates a floating-point number to the nearest 32-bit signed integer, rounding towards zero.
If the `Float` is larger than the maximum value for `Int32` (including `Inf`), returns the maximum
value of `Int32` (i.e. `Int32.maxValue`). If it is smaller than the minimum value for `Int32`
(including `-Inf`), returns the minimum value of `Int32` (i.e. `Int32.minValue`). If it is `NaN`,
returns `0`.
This function does not reduce in the kernel.
-/
@[extern "lean_float_to_int32"] opaque Float.toInt32 : Float → Int32
/--
Truncates the value to the nearest integer, rounding towards zero.
If NaN, returns `0`.
If larger than the maximum value for `Int64` (including Inf), returns the maximum value of `Int64`
(i.e. `Int64.maxValue`).
If smaller than the minimum value for `Int64` (including -Inf), returns the minimum value of `Int64`
(i.e. `Int64.minValue`).
Truncates a floating-point number to the nearest 64-bit signed integer, rounding towards zero.
If the `Float` is larger than the maximum value for `Int64` (including `Inf`), returns the maximum
value of `Int64` (i.e. `Int64.maxValue`). If it is smaller than the minimum value for `Int64`
(including `-Inf`), returns the minimum value of `Int64` (i.e. `Int64.minValue`). If it is `NaN`,
returns `0`.
This function does not reduce in the kernel.
-/
@[extern "lean_float_to_int64"] opaque Float.toInt64 : Float → Int64
/--
Truncates the value to the nearest integer, rounding towards zero.
If NaN, returns `0`.
If larger than the maximum value for `ISize` (including Inf), returns the maximum value of `ISize`
(i.e. `ISize.maxValue`).
If smaller than the minimum value for `ISize` (including -Inf), returns the minimum value of `ISize`
(i.e. `ISize.minValue`).
Truncates a floating-point number to the nearest word-sized signed integer, rounding towards zero.
If the `Float` is larger than the maximum value for `ISize` (including `Inf`), returns the maximum
value of `ISize` (i.e. `ISize.maxValue`). If it is smaller than the minimum value for `ISize`
(including `-Inf`), returns the minimum value of `ISize` (i.e. `ISize.minValue`). If it is `NaN`,
returns `0`.
This function does not reduce in the kernel.
-/
@[extern "lean_float_to_isize"] opaque Float.toISize : Float → ISize
/-- Obtains the `Float` whose value is the same as the given `Int8`. -/
/--
Obtains the `Float` whose value is the same as the given `Int8`.
This function does not reduce in the kernel.
-/
@[extern "lean_int8_to_float"] opaque Int8.toFloat (n : Int8) : Float
/-- Obtains the `Float` whose value is the same as the given `Int16`. -/
/--
Obtains the `Float` whose value is the same as the given `Int16`.
This function does not reduce in the kernel.
-/
@[extern "lean_int16_to_float"] opaque Int16.toFloat (n : Int16) : Float
/-- Obtains the `Float` whose value is the same as the given `Int32`. -/
/--
Obtains the `Float` whose value is the same as the given `Int32`.
This function does not reduce in the kernel.
-/
@[extern "lean_int32_to_float"] opaque Int32.toFloat (n : Int32) : Float
/--
Obtains a `Float` whose value is near the given `Int64`.
@ -68,8 +89,8 @@ It will be exactly the value of the given `Int64` if such a `Float` exists. If n
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.
This function does not reduce in the kernel.
-/
@[extern "lean_int64_to_float"] opaque Int64.toFloat (n : Int64) : Float
/--
@ -79,7 +100,6 @@ It will be exactly the value of the given `ISize` if such a `Float` exists. If n
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.
This function does not reduce in the kernel.
-/
@[extern "lean_isize_to_float"] opaque ISize.toFloat (n : ISize) : Float

87
src/Init/Data/SInt/Float32.lean
View file

@ -10,54 +10,71 @@ import Init.Data.SInt.Basic
set_option linter.missingDocs true
/--
Truncates the value to the nearest integer, rounding towards zero.
If NaN, returns `0`.
If larger than the maximum value for `Int8` (including Inf), returns the maximum value of `Int8`
(i.e. `Int8.maxValue`).
If smaller than the minimum value for `Int8` (including -Inf), returns the minimum value of `Int8`
(i.e. `Int8.minValue`).
Truncates a floating-point number to the nearest 8-bit signed integer, rounding towards zero.
If the `Float` is larger than the maximum value for `Int8` (including `Inf`), returns the maximum value of
`Int8` (i.e. `Int8.maxValue`). If it is smaller than the minimum value for `Int8` (including `-Inf`),
returns the minimum value of `Int8` (i.e. `Int8.minValue`). If it is `NaN`, returns `0`.
This function does not reduce in the kernel.
-/
@[extern "lean_float32_to_int8"] opaque Float32.toInt8 : Float32 → Int8
/--
Truncates the value to the nearest integer, rounding towards zero.
If NaN, returns `0`.
If larger than the maximum value for `Int16` (including Inf), returns the maximum value of `Int16`
(i.e. `Int16.maxValue`).
If smaller than the minimum value for `Int16` (including -Inf), returns the minimum value of `Int16`
(i.e. `Int16.minValue`).
Truncates a floating-point number to the nearest 16-bit signed integer, rounding towards zero.
If the `Float` is larger than the maximum value for `Int16` (including `Inf`), returns the maximum
value of `Int16` (i.e. `Int16.maxValue`). If it is smaller than the minimum value for `Int16`
(including `-Inf`), returns the minimum value of `Int16` (i.e. `Int16.minValue`). If it is `NaN`,
returns `0`.
This function does not reduce in the kernel.
-/
@[extern "lean_float32_to_int16"] opaque Float32.toInt16 : Float32 → Int16
/--
Truncates the value to the nearest integer, rounding towards zero.
If NaN, returns `0`.
If larger than the maximum value for `Int32` (including Inf), returns the maximum value of `Int32`
(i.e. `Int32.maxValue`).
If smaller than the minimum value for `Int32` (including -Inf), returns the minimum value of `Int32`
(i.e. `Int32.minValue`).
Truncates a floating-point number to the nearest 32-bit signed integer, rounding towards zero.
If the `Float` is larger than the maximum value for `Int32` (including `Inf`), returns the maximum
value of `Int32` (i.e. `Int32.maxValue`). If it is smaller than the minimum value for `Int32`
(including `-Inf`), returns the minimum value of `Int32` (i.e. `Int32.minValue`). If it is `NaN`,
returns `0`.
This function does not reduce in the kernel.
-/
@[extern "lean_float32_to_int32"] opaque Float32.toInt32 : Float32 → Int32
/--
Truncates the value to the nearest integer, rounding towards zero.
If NaN, returns `0`.
If larger than the maximum value for `Int64` (including Inf), returns the maximum value of `Int64`
(i.e. `Int64.maxValue`).
If smaller than the minimum value for `Int64` (including -Inf), returns the minimum value of `Int64`
(i.e. `Int64.minValue`).
Truncates a floating-point number to the nearest 64-bit signed integer, rounding towards zero.
If the `Float` is larger than the maximum value for `Int64` (including `Inf`), returns the maximum
value of `Int64` (i.e. `Int64.maxValue`). If it is smaller than the minimum value for `Int64`
(including `-Inf`), returns the minimum value of `Int64` (i.e. `Int64.minValue`). If it is `NaN`,
returns `0`.
This function does not reduce in the kernel.
-/
@[extern "lean_float32_to_int64"] opaque Float32.toInt64 : Float32 → Int64
/--
Truncates the value to the nearest integer, rounding towards zero.
If NaN, returns `0`.
If larger than the maximum value for `ISize` (including Inf), returns the maximum value of `ISize`
(i.e. `ISize.maxValue`).
If smaller than the minimum value for `ISize` (including -Inf), returns the minimum value of `ISize`
(i.e. `ISize.minValue`).
Truncates a floating-point number to the nearest word-sized signed integer, rounding towards zero.
If the `Float` is larger than the maximum value for `ISize` (including `Inf`), returns the maximum
value of `ISize` (i.e. `ISize.maxValue`). If it is smaller than the minimum value for `ISize`
(including `-Inf`), returns the minimum value of `ISize` (i.e. `ISize.minValue`). If it is `NaN`,
returns `0`.
This function does not reduce in the kernel.
-/
@[extern "lean_float32_to_isize"] opaque Float32.toISize : Float32 → ISize
/-- Obtains the `Float32` whose value is the same as the given `Int8`. -/
/--
Obtains the `Float32` whose value is the same as the given `Int8`.
This function does not reduce in the kernel.
-/
@[extern "lean_int8_to_float32"] opaque Int8.toFloat32 (n : Int8) : Float32
/-- Obtains the `Float32` whose value is the same as the given `Int16`. -/
/--
Obtains the `Float32` whose value is the same as the given `Int16`.
This function does not reduce in the kernel.
-/
@[extern "lean_int16_to_float32"] opaque Int16.toFloat32 (n : Int16) : Float32
/--
Obtains a `Float32` whose value is near the given `Int32`.
@ -65,6 +82,8 @@ Obtains a `Float32` whose value is near the given `Int32`.
It will be exactly the value of the given `Int32` 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 does not reduce in the kernel.
-/
@[extern "lean_int32_to_float32"] opaque Int32.toFloat32 (n : Int32) : Float32
/--
@ -73,6 +92,8 @@ Obtains a `Float32` whose value is near the given `Int64`.
It will be exactly the value of the given `Int64` 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 does not reduce in the kernel.
-/
@[extern "lean_int64_to_float32"] opaque Int64.toFloat32 (n : Int64) : Float32
/--
@ -81,5 +102,7 @@ Obtains a `Float32` whose value is near the given `ISize`.
It will be exactly the value of the given `ISize` 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 does not reduce in the kernel.
-/
@[extern "lean_isize_to_float32"] opaque ISize.toFloat32 (n : ISize) : Float32