From 0d1d8b69445161ead759c6aa642d689320cb7327 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Wed, 26 Mar 2025 06:25:06 +0100 Subject: [PATCH] doc: review docstrings for Float and Float32 (#7642) This PR reviews the docstrings for `Float` and `Float32`, adding missing ones and making their format consistent. --- src/Init/Data/Float.lean | 362 +++++++++++++++++++++++++++---- src/Init/Data/Float32.lean | 365 +++++++++++++++++++++++++++++--- src/Init/Data/OfScientific.lean | 26 ++- src/Init/Data/SInt/Float.lean | 94 ++++---- src/Init/Data/SInt/Float32.lean | 87 +++++--- 5 files changed, 791 insertions(+), 143 deletions(-) diff --git a/src/Init/Data/Float.lean b/src/Init/Data/Float.lean index 5a66ab696b..74350a4f0f 100644 --- a/src/Init/Data/Float.lean +++ b/src/Init/Data/Float.lean @@ -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 diff --git a/src/Init/Data/Float32.lean b/src/Init/Data/Float32.lean index af1ac82a74..092d1e1219 100644 --- a/src/Init/Data/Float32.lean +++ b/src/Init/Data/Float32.lean @@ -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 diff --git a/src/Init/Data/OfScientific.lean b/src/Init/Data/OfScientific.lean index 21d232f036..4c044c876e 100644 --- a/src/Init/Data/OfScientific.lean +++ b/src/Init/Data/OfScientific.lean @@ -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)) diff --git a/src/Init/Data/SInt/Float.lean b/src/Init/Data/SInt/Float.lean index 374fcf0fe2..08f06c0924 100644 --- a/src/Init/Data/SInt/Float.lean +++ b/src/Init/Data/SInt/Float.lean @@ -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 diff --git a/src/Init/Data/SInt/Float32.lean b/src/Init/Data/SInt/Float32.lean index c0bda27897..1161a1f17c 100644 --- a/src/Init/Data/SInt/Float32.lean +++ b/src/Init/Data/SInt/Float32.lean @@ -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