Lean ่ฏญ่จ€ๅ‚่€ƒ

20.6.ย ๆตฎ็‚นๆ•ฐ๐Ÿ”—

ๆตฎ็‚นๆ•ฐๆ˜ฏๅœจ่ฎก็ฎ—ๆœบ็กฌไปถไธญๆœ‰ๆ•ˆๅฎž็Žฐ็š„ๅฎžๆ•ฐ็š„่ฟ‘ไผผๅ€ผใ€‚ ไฝฟ็”จๆตฎ็‚นๆ•ฐ็š„่ฎก็ฎ—้žๅธธ้ซ˜ๆ•ˆ๏ผ›็„ถ่€Œ๏ผŒๅฎƒไปฌ่ฟ‘ไผผๅฎžๆ•ฐ็š„ๆ–นๅผ็š„ๆ€ง่ดจๅพˆๅคๆ‚๏ผŒๅญ˜ๅœจ่ฎธๅคšๆž็ซฏๆƒ…ๅ†ตใ€‚ IEEE 754 ๆ ‡ๅ‡†ๅฎšไน‰ไบ†็Žฐไปฃ่ฎก็ฎ—ๆœบไธŠไฝฟ็”จ็š„ๆตฎ็‚นๆ ผๅผ๏ผŒๅ…่ฎธ็กฌไปถ่ฎพ่ฎกไบบๅ‘˜ๅšๅ‡บๆŸไบ›้€‰ๆ‹ฉ๏ผŒ่€Œๅฎž้™…็ณป็ปŸๅœจ่ฟ™ไบ›ๅฐ็ป†่Š‚ไธŠๆœ‰ๆ‰€ไธๅŒใ€‚ ไพ‹ๅฆ‚๏ผŒNaN ๆœ‰่ฎธๅคšไธๅŒ็š„ไฝ่กจ็คบ๏ผŒ็ป“ๆžœๆœชๅฎšไน‰็š„ๆŒ‡็คบ็ฌฆ๏ผŒๅนถไธ”ๆŸไบ›ๅนณๅฐๅœจ้€š่ฟ‡ๆทปๅŠ ไธคไธช NaN ่ฟ”ๅ›ž็š„ NaN ๆ–น้ขๆœ‰ๆ‰€ไธๅŒใ€‚

Lean ๅ…ฌๅผ€ๅบ•ๅฑ‚ๅนณๅฐ็š„ๆตฎ็‚นๅ€ผไปฅไพ›็ผ–็จ‹ไฝฟ็”จ๏ผŒไฝ†ๅฎƒไปฌๆœชๅœจ Lean ็š„้€ป่พ‘ไธญ่ฟ›่กŒ็ผ–็ ใ€‚ ๅฎƒไปฌ็”ฑไธ้€ๆ˜Ž็ฑปๅž‹่กจ็คบใ€‚ ่ฟ™ๆ„ๅ‘ณ็€๏ผŒๅฆ‚ๆžœๆฒกๆœ‰้ขๅค–็š„ ๅ…ฌ็†๏ผŒๅ†…ๆ ธ ๆ— ๆณ•ไฝฟ็”จๆตฎ็‚นๅ€ผ่ฟ›่กŒ่ฎก็ฎ—ๆˆ–ๆŽจ็†ใ€‚ ่ฟ™ๆ ทๅš็š„็ป“ๆžœๆ˜ฏๆตฎ็‚นๆ•ฐ็š„็›ธ็ญ‰ๆ€งๆ˜ฏไธๅฏๅˆคๅฎš็š„ใ€‚ ๆญคๅค–๏ผŒๆตฎ็‚นๅ€ผไน‹้—ด็š„ๆฏ”่พƒๆ˜ฏๅฏๅˆคๅฎš็š„๏ผŒไฝ†่ฟ™ๆ ทๅš็š„ไปฃ็ ๆ˜ฏไธ้€ๆ˜Ž็š„๏ผ›ๅฎž้™…ไธŠ๏ผŒๅ†ณ็ญ–่ฟ‡็จ‹ๅช่ƒฝๅœจ็ผ–่ฏ‘ไปฃ็ ไธญไฝฟ็”จใ€‚

Lean ๆไพ›ไธค็งๆตฎ็‚น็ฑปๅž‹๏ผšFloat ่กจ็คบ 64 ไฝๆตฎ็‚นๅ€ผ๏ผŒ่€Œ Float32 ่กจ็คบ 32 ไฝๆตฎ็‚นๅ€ผใ€‚ Float ็š„็ฒพๅบฆไธไผšๅ›  Lean ่ฟ่กŒ็š„ๅนณๅฐ่€Œๅผ‚ใ€‚

๐Ÿ”—type
Float : Type
Float : Type

64-bit floating-point numbers.

Float corresponds to the IEEE 754 binary64 format (double in C or f64 in Rust). Floating-point numbers are a finite representation of a subset of the real numbers, extended with extra โ€œsentinelโ€ values that represent undefined and infinite results as well as separate positive and negative zeroes. Arithmetic on floating-point numbers approximates the corresponding operations on the real numbers by rounding the results to numbers that are representable, propagating error and infinite values.

Floating-point numbers include subnormal numbers. Their special values are:

  • NaN, which denotes a class of โ€œnot a numberโ€ values that result from operations such as dividing zero by zero, and

  • Inf and -Inf, which represent positive and infinities that result from dividing non-zero values by zero.

๐Ÿ”—type
Float32 : Type
Float32 : Type

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

No Kernel Reasoning About Floating-Point Numbers

Leanๅ†…ๆ ธๅฏไปฅๆฏ”่พƒ Float ็ฑปๅž‹็š„่กจ่พพๅผ็š„่ฏญๆณ•็›ธ็ญ‰ๆ€ง๏ผŒๅ› ๆญค 0.0 ๅœจๅฎšไน‰ไธŠ็ญ‰ไบŽๅ…ถ่‡ช่บซใ€‚

example : (0.0 : Float) = (0.0 : Float) := โŠข 0.0 = 0.0 All goals completed! ๐Ÿ™

ๅ†…ๆ ธๆ— ๆณ•ๆฃ€ๆŸฅ้œ€่ฆๅฝ’็บฆๆ‰่ƒฝๅœจ่ฏญๆณ•ไธŠ็›ธ็ญ‰็š„ๆœฏ่ฏญ๏ผš

example : (0.0 : Float) = (0.0 + 0.0 : Float) := โŠข 0.0 = 0.0 + 0.0 Tactic `rfl` failed: The left-hand side 0.0 is not definitionally equal to the right-hand side 0.0 + 0.0 โŠข 0.0 = 0.0 + 0.0โŠข 0.0 = 0.0 + 0.0 
Tactic `rfl` failed: The left-hand side
  0.0
is not definitionally equal to the right-hand side
  0.0 + 0.0

โŠข 0.0 = 0.0 + 0.0

ๅŒๆ ท๏ผŒๅ†…ๆ ธๅœจๆฃ€ๆŸฅ ๅฎšไน‰็ญ‰ไปท ๆ—ถๆ— ๆณ•่ฏ„ไผฐๆตฎ็‚นๆ•ฐ็š„ Bool ๅ€ผๆฏ”่พƒ๏ผš

theorem Float.zero_eq_zero_plus_zero : ((0.0 : Float) == (0.0 + 0.0 : Float)) = true := โŠข (0.0 == 0.0 + 0.0) = true Tactic `rfl` failed: The left-hand side 0.0 == 0.0 + 0.0 is not definitionally equal to the right-hand side true โŠข (0.0 == 0.0 + 0.0) = trueโŠข (0.0 == 0.0 + 0.0) = true 
Tactic `rfl` failed: The left-hand side
  0.0 == 0.0 + 0.0
is not definitionally equal to the right-hand side
  true

โŠข (0.0 == 0.0 + 0.0) = true

ไฝ†ๆ˜ฏ๏ผŒnative_decide็ญ–็•ฅๅฏไปฅ่ฐƒ็”จ Lean ็”จไบŽ่ฟ่กŒๆ—ถ็จ‹ๅบ็š„ๅบ•ๅฑ‚ๅนณๅฐ็š„ๆตฎ็‚นๅŽŸ่ฏญ๏ผš

theorem Float.zero_eq_zero_plus_zero : ((0.0 : Float) == (0.0 + 0.0 : Float)) = true := โŠข (0.0 == 0.0 + 0.0) = true All goals completed! ๐Ÿ™

่ฏฅ็ญ–็•ฅๅฐ†ๅ†ณ็ญ–่ฟ‡็จ‹ไฝœไธบๅทฒ็ผ–่ฏ‘็š„ๆœฌๆœบไปฃ็ ๆ‰ง่กŒใ€‚ ้™คไบ†ๅ†…ๆ ธไน‹ๅค–๏ผŒ่ฟ™่ฟ˜้œ€่ฆไฟกไปป Lean ็ผ–่ฏ‘ๅ™จใ€่งฃ้‡Šๅ™จๅ’Œๅ†…็ฝฎ่ฟ็ฎ—็ฌฆ็š„ไฝŽ็บงๅฎž็Žฐใ€‚ ไธบไบ†็ฒพ็กฎๅœฐ้˜ๆ˜Ž่ฟ™็งไพ่ต–ๆ€ง๏ผŒ็ญ–็•ฅๅˆ›ๅปบไบ†ๅ…ฌ็† Float.zero_eq_zero_plus_zero._native.native_decide.ax_1๏ผš

'Float.zero_eq_zero_plus_zero' depends on axioms: [Classical.choice, Float.zero_eq_zero_plus_zero._native.native_decide.ax_1]#print axioms Float.zero_eq_zero_plus_zero 
'Float.zero_eq_zero_plus_zero' depends on axioms: [Classical.choice,
 Float.zero_eq_zero_plus_zero._native.native_decide.ax_1]
Live โ†ช
Floating-Point Equality Is Not Reflexive

ๆตฎ็‚น่ฟ็ฎ—ๅฏ่ƒฝไผšไบง็”ŸๆŒ‡็คบๆœชๅฎšไน‰็ป“ๆžœ็š„ NaN ๅ€ผใ€‚ ่ฟ™ไบ›ๅ€ผๅฝผๆญคไน‹้—ดๆฒกๆœ‰ๅฏๆฏ”ๆ€ง๏ผ›็‰นๅˆซๆ˜ฏ๏ผŒๆถ‰ๅŠ NaN ็š„ๆ‰€ๆœ‰ๆฏ”่พƒ้ƒฝๅฐ†่ฟ”ๅ›ž false๏ผŒๅŒ…ๆ‹ฌ็›ธ็ญ‰ใ€‚

false#eval ((0.0 : Float) / 0.0) == ((0.0 : Float) / 0.0)
Live โ†ช
Floating-Point Equality Is Not a Congruence

ๅฐ†ๅ‡ฝๆ•ฐๅบ”็”จไบŽไธคไธช็›ธ็ญ‰็š„ๆตฎ็‚นๆ•ฐๅฏ่ƒฝไธไผšไบง็”Ÿ็›ธ็ญ‰็š„ๆ•ฐๅญ—ใ€‚ ็‰นๅˆซๆ˜ฏ๏ผŒๆญฃ้›ถๅ’Œ่ดŸ้›ถๆ˜ฏ้€š่ฟ‡ๆตฎ็‚น็›ธ็ญ‰็›ธ็ญ‰็š„ไธๅŒๅ€ผ๏ผŒไฝ†้™คไปฅๆญฃ้›ถๆˆ–่ดŸ้›ถไผšไบง็”Ÿๆญฃๆ— ็ฉทๅคงๅ€ผๆˆ–่ดŸๆ— ็ฉทๅคงๅ€ผใ€‚

def neg0 : Float := -0.0 def pos0 : Float := 0.0 (true, false)#eval (neg0 == pos0, 1.0 / neg0 == 1.0 / pos0) 
(true, false)
Live โ†ช

20.6.1.ย ๅฅๆณ•๐Ÿ”—

Lean ๆฒกๆœ‰ไธ“็”จ็š„ๆตฎ็‚นๆ–‡ๅญ—ใ€‚ ็›ธๅ๏ผŒๆตฎ็‚นๆ–‡ๅญ—ๆ˜ฏ้€š่ฟ‡ OfScientific ๅ’Œ Neg ็ฑปๅž‹็ฑป็š„้€‚ๅฝ“ๅฎžไพ‹ๆฅ่งฃๆž็š„ใ€‚

Floating-Point Literals

ๆœŸ้™

(-2.523 : Float)

ๆ˜ฏ่ฏญๆณ•็ณ–

(Neg.neg (OfScientific.ofScientific 22523 true 4) : Float)

ๅ’Œๆœฏ่ฏญ

(413.52 : Float32)

ๆ˜ฏ่ฏญๆณ•็ณ–

(OfScientific.ofScientific 41352 true 2 : Float32)
Live โ†ช

20.6.2.ย API ๅ‚่€ƒ๐Ÿ”—

20.6.2.1.ย ็‰นๆ€ง๐Ÿ”—

ๆตฎ็‚นๆ•ฐๅฑžไบŽไปฅไธ‹ไธ‰็ฑปไน‹ไธ€๏ผš

  • ๆœ‰้™ๆ•ฐๆ˜ฏๆ™ฎ้€š็š„ๆตฎ็‚นๅ€ผใ€‚

  • ๆ— ็ฉทๅคง๏ผˆๅฏไปฅๆ˜ฏๆญฃๆ•ฐๆˆ–่ดŸๆ•ฐ๏ผ‰ๆ˜ฏ้™คไปฅ้›ถ็š„็ป“ๆžœใ€‚

  • NaN ไธๆ˜ฏๆ•ฐๅญ—๏ผŒๆ˜ฏๅ…ถไป–ๆœชๅฎšไน‰่ฟ็ฎ—็š„็ป“ๆžœ๏ผŒไพ‹ๅฆ‚่ดŸๆ•ฐ็š„ๅนณๆ–นๆ นใ€‚

๐Ÿ”—opaque
Float.isInf : Float โ†’ Bool
Float.isInf : Float โ†’ Bool

Checks whether a floating-point number is a positive or negative infinite number, but not a finite number or NaN.

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

๐Ÿ”—opaque
Float32.isInf : Float32 โ†’ Bool
Float32.isInf : 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.

๐Ÿ”—opaque
Float.isNaN : Float โ†’ Bool
Float.isNaN : Float โ†’ Bool

Checks whether a floating point number is NaN (โ€œnot a numberโ€) value.

NaN values result from operations that might otherwise be errors, such as dividing zero by zero.

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

๐Ÿ”—opaque
Float32.isNaN : Float32 โ†’ Bool
Float32.isNaN : Float32 โ†’ Bool

Checks whether a floating point number is NaN ("not a number") value.

NaN values result from operations that might otherwise be errors, such as dividing zero by zero.

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

๐Ÿ”—opaque
Float.isFinite : Float โ†’ Bool
Float.isFinite : Float โ†’ Bool

Checks whether a floating-point number is finite, that is, whether it is normal, subnormal, or zero, but not infinite or NaN.

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

๐Ÿ”—opaque
Float32.isFinite : Float32 โ†’ Bool
Float32.isFinite : 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.

20.6.2.2.ย ๅฅๆณ•๐Ÿ”—

่ฟ™ไบ›ๆ“ไฝœ็š„ๅญ˜ๅœจๆ˜ฏไธบไบ†ๆ”ฏๆŒ OfScientific Float ๅ’Œ OfScientific Float32 ๅฎžไพ‹๏ผŒๅนถไธ”้€šๅธธไฝœไธบๆ–‡ๅญ—ๅ€ผ็š„็ป“ๆžœ้—ดๆŽฅ่ฐƒ็”จใ€‚

๐Ÿ”—opaque
Float.ofScientific (m : Nat) (s : Bool) (e : Nat) : Float
Float.ofScientific (m : Nat) (s : Bool)
  (e : Nat) : Float

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.

๐Ÿ”—opaque
Float32.ofScientific (m : Nat) (s : Bool) (e : Nat) : Float32
Float32.ofScientific (m : Nat) (s : Bool)
  (e : Nat) : Float32

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.

20.6.2.3.ย ่ฝฌๆข๐Ÿ”—

๐Ÿ”—opaque
Float.toBits : Float โ†’ UInt64
Float.toBits : Float โ†’ UInt64

Bit-for-bit conversion to UInt64. Interprets a Float as a UInt64, ignoring the numeric value and treating the Float's bit pattern as a UInt64.

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

This function is distinct from Float.toUInt64, which attempts to preserve the numeric value rather than reinterpreting the bit pattern.

๐Ÿ”—opaque
Float32.toBits : Float32 โ†’ UInt32
Float32.toBits : Float32 โ†’ 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 UInt32s have the same endianness on all supported platforms. IEEE 754 very precisely specifies the bit layout of floats.

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.

๐Ÿ”—opaque
Float.ofBits : UInt64 โ†’ Float
Float.ofBits : UInt64 โ†’ Float

Bit-for-bit conversion from UInt64. Interprets a UInt64 as a Float, ignoring the numeric value and treating the UInt64's bit pattern as a Float.

Floats and UInt64s 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.

๐Ÿ”—opaque
Float32.ofBits : UInt32 โ†’ Float32
Float32.ofBits : UInt32 โ†’ Float32

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 UInt32s 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.

๐Ÿ”—opaque
Float.toFloat32 : Float โ†’ Float32
Float.toFloat32 : Float โ†’ Float32

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.

๐Ÿ”—opaque
Float32.toFloat : Float32 โ†’ Float
Float32.toFloat : Float32 โ†’ Float

Converts a 32-bit floating-point number to a 64-bit floating-point number.

This function does not reduce in the kernel.

๐Ÿ”—opaque
Float.toString : Float โ†’ String
Float.toString : Float โ†’ String

Converts a floating-point number to a string.

This function does not reduce in the kernel.

๐Ÿ”—opaque
Float32.toString : Float32 โ†’ String
Float32.toString : Float32 โ†’ String

Converts a floating-point number to a string.

This function does not reduce in the kernel.

๐Ÿ”—opaque
Float.toUInt8 : Float โ†’ UInt8
Float.toUInt8 : Float โ†’ UInt8

Converts a floating-point number to an 8-bit unsigned integer.

If the given Float is non-negative, truncates the value to a positive integer, rounding down and clamping to the range of UInt8. Returns 0 if the Float is negative or NaN, and returns the largest UInt8 value (i.e. UInt8.size - 1) if the float is larger than it.

This function does not reduce in the kernel.

๐Ÿ”—opaque
Float.toInt8 : Float โ†’ Int8
Float.toInt8 : Float โ†’ Int8

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.

๐Ÿ”—opaque
Float32.toUInt8 : Float32 โ†’ UInt8
Float32.toUInt8 : Float32 โ†’ UInt8

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.

๐Ÿ”—opaque
Float32.toInt8 : Float32 โ†’ Int8
Float32.toInt8 : Float32 โ†’ Int8

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.

๐Ÿ”—opaque
Float.toUInt16 : Float โ†’ UInt16
Float.toUInt16 : Float โ†’ UInt16

Converts a floating-point number to a 16-bit unsigned integer.

If the given Float is non-negative, truncates the value to a positive integer, rounding down and clamping to the range of UInt16. Returns 0 if the Float is negative or NaN, and returns the largest UInt16 value (i.e. UInt16.size - 1) if the float is larger than it.

This function does not reduce in the kernel.

๐Ÿ”—opaque
Float.toInt16 : Float โ†’ Int16
Float.toInt16 : Float โ†’ Int16

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.

๐Ÿ”—opaque
Float32.toUInt16 : Float32 โ†’ UInt16
Float32.toUInt16 : Float32 โ†’ UInt16

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.

๐Ÿ”—opaque
Float32.toInt16 : Float32 โ†’ Int16
Float32.toInt16 : Float32 โ†’ Int16

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.

๐Ÿ”—opaque
Float.toUInt32 : Float โ†’ UInt32
Float.toUInt32 : Float โ†’ UInt32

Converts a floating-point number to a 32-bit unsigned integer.

If the given Float is non-negative, truncates the value to a positive integer, rounding down and clamping to the range of UInt32. Returns 0 if the Float is negative or NaN, and returns the largest UInt32 value (i.e. UInt32.size - 1) if the float is larger than it.

This function does not reduce in the kernel.

๐Ÿ”—opaque
Float32.toUInt32 : Float32 โ†’ UInt32
Float32.toUInt32 : Float32 โ†’ UInt32

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.

๐Ÿ”—opaque
Float.toInt32 : Float โ†’ Int32
Float.toInt32 : Float โ†’ Int32

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.

๐Ÿ”—opaque
Float32.toInt32 : Float32 โ†’ Int32
Float32.toInt32 : Float32 โ†’ Int32

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.

๐Ÿ”—opaque
Float.toUInt64 : Float โ†’ UInt64
Float.toUInt64 : Float โ†’ UInt64

Converts a floating-point number to a 64-bit unsigned integer.

If the given Float is non-negative, truncates the value to a positive integer, rounding down and clamping to the range of UInt64. Returns 0 if the Float is negative or NaN, and returns the largest UInt64 value (i.e. UInt64.size - 1) if the float is larger than it.

This function does not reduce in the kernel.

๐Ÿ”—opaque
Float.toInt64 : Float โ†’ Int64
Float.toInt64 : Float โ†’ Int64

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.

๐Ÿ”—opaque
Float32.toUInt64 : Float32 โ†’ UInt64
Float32.toUInt64 : Float32 โ†’ UInt64

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.

๐Ÿ”—opaque
Float32.toInt64 : Float32 โ†’ Int64
Float32.toInt64 : Float32 โ†’ Int64

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.

๐Ÿ”—opaque
Float.toUSize : Float โ†’ USize
Float.toUSize : Float โ†’ USize

Converts a floating-point number to a word-sized unsigned integer.

If the given Float is non-negative, truncates the value to a positive integer, rounding down and clamping to the range of USize. Returns 0 if the Float is negative or NaN, and returns the largest USize value (i.e. USize.size - 1) if the float is larger than it.

This function does not reduce in the kernel.

๐Ÿ”—opaque
Float32.toUSize : Float32 โ†’ USize
Float32.toUSize : Float32 โ†’ USize

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.

๐Ÿ”—opaque
Float.toISize : Float โ†’ ISize
Float.toISize : Float โ†’ ISize

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.

๐Ÿ”—opaque
Float32.toISize : Float32 โ†’ ISize
Float32.toISize : Float32 โ†’ ISize

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.

๐Ÿ”—def
Float.ofInt : Int โ†’ Float
Float.ofInt : Int โ†’ Float

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
Float32.ofInt : Int โ†’ Float32
Float32.ofInt : Int โ†’ Float32

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
Float.ofNat (n : Nat) : Float
Float.ofNat (n : Nat) : Float

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.

๐Ÿ”—def
Float32.ofNat (n : Nat) : Float32
Float32.ofNat (n : Nat) : Float32

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.

๐Ÿ”—def
Float.ofBinaryScientific (m : Nat) (e : Int) : Float
Float.ofBinaryScientific (m : Nat)
  (e : Int) : Float

Computes m * 2^e.

๐Ÿ”—def
Float32.ofBinaryScientific (m : Nat) (e : Int) : Float32
Float32.ofBinaryScientific (m : Nat)
  (e : Int) : Float32

Computes m * 2^e.

๐Ÿ”—opaque
Float.frExp : Float โ†’ Float ร— Int
Float.frExp : Float โ†’ Float ร— Int

Splits the given float x into a significand/exponent pair (s, i) such that x = s * 2^i where s โˆˆ (-1;-0.5] โˆช [0.5; 1). Returns an undefined value if x is not finite.

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

๐Ÿ”—opaque
Float32.frExp : Float32 โ†’ Float32 ร— Int
Float32.frExp : Float32 โ†’ Float32 ร— Int

Splits the given float x into a significand/exponent pair (s, i) such that x = s * 2^i where s โˆˆ (-1;-0.5] โˆช [0.5; 1). Returns an undefined value if x is not finite.

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

20.6.2.4.ย ๆฏ”่พƒ๐Ÿ”—

๐Ÿ”—opaque
Float.beq (a b : Float) : Bool
Float.beq (a b : Float) : Bool

Checks whether two floating-point numbers are equal according to IEEE 754.

Floating-point equality does not correspond with propositional equality. In particular, it is not reflexive since NaN != NaN, and it is not a congruence because 0.0 == -0.0, but 1.0 / 0.0 != 1.0 / -0.0.

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

๐Ÿ”—opaque
Float32.beq (a b : Float32) : Bool
Float32.beq (a b : Float32) : Bool

Checks whether two floating-point numbers are equal according to IEEE 754.

Floating-point equality does not correspond with propositional equality. In particular, it is not reflexive since NaN != NaN, and it is not a congruence because 0.0 == -0.0, but 1.0 / 0.0 != 1.0 / -0.0.

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

20.6.2.4.1.ย ไธๅนณ็ญ‰็Žฐ่ฑก๐Ÿ”—

ไธ็ญ‰ๅผ็š„ๅ†ณ็ญ–่ฟ‡็จ‹ๆ˜ฏ้€ป่พ‘ไธญไธ้€ๆ˜Ž็š„ๅธธๆ•ฐใ€‚ ๅฎƒไปฌๅช่ƒฝ้€š่ฟ‡ Lean.ofReduceBool ๅ…ฌ็†ไฝฟ็”จ๏ผŒไพ‹ๅฆ‚้€š่ฟ‡ native_decide็ญ–็•ฅใ€‚

๐Ÿ”—def
Float.le : Float โ†’ Float โ†’ Prop
Float.le : Float โ†’ Float โ†’ Prop

Non-strict inequality of floating-point numbers. Typically used via the โ‰ค operator.

๐Ÿ”—def
Float32.le : Float32 โ†’ Float32 โ†’ Prop
Float32.le : Float32 โ†’ Float32 โ†’ Prop

Non-strict inequality of floating-point numbers. Typically used via the โ‰ค operator.

๐Ÿ”—def
Float.lt : Float โ†’ Float โ†’ Prop
Float.lt : Float โ†’ Float โ†’ Prop

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

๐Ÿ”—def
Float32.lt : Float32 โ†’ Float32 โ†’ Prop
Float32.lt : Float32 โ†’ Float32 โ†’ Prop

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

๐Ÿ”—opaque
Float.decLe (a b : Float) : Decidable (a โ‰ค b)
Float.decLe (a b : Float) :
  Decidable (a โ‰ค b)

Compares two floating point numbers for non-strict inequality.

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

๐Ÿ”—opaque
Float32.decLe (a b : Float32) : Decidable (a โ‰ค b)
Float32.decLe (a b : Float32) :
  Decidable (a โ‰ค b)

Compares two floating point numbers for non-strict inequality.

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

๐Ÿ”—opaque
Float.decLt (a b : Float) : Decidable (a < b)
Float.decLt (a b : Float) :
  Decidable (a < b)

Compares two floating point numbers for strict inequality.

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

๐Ÿ”—opaque
Float32.decLt (a b : Float32) : Decidable (a < b)
Float32.decLt (a b : Float32) :
  Decidable (a < b)

Compares two floating point numbers for strict inequality.

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

20.6.2.5.ย ็ฎ—ๆœฏ๐Ÿ”—

ๆตฎ็‚นๅ€ผ็š„็ฎ—ๆœฏ่ฟ็ฎ—้€šๅธธ้€š่ฟ‡ Add Floatใ€Sub Floatใ€Mul Floatใ€Div Float ๅ’Œ HomogeneousPow Float ๅฎžไพ‹ไปฅๅŠ็›ธๅบ”็š„ Float32 ๅฎžไพ‹่ฐƒ็”จใ€‚

๐Ÿ”—opaque
Float.add : Float โ†’ Float โ†’ Float
Float.add : Float โ†’ Float โ†’ Float

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

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

๐Ÿ”—opaque
Float32.add : Float32 โ†’ Float32 โ†’ Float32
Float32.add : Float32 โ†’ Float32 โ†’ Float32

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.

๐Ÿ”—opaque
Float.sub : Float โ†’ Float โ†’ Float
Float.sub : Float โ†’ Float โ†’ Float

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

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

๐Ÿ”—opaque
Float32.sub : Float32 โ†’ Float32 โ†’ Float32
Float32.sub : 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.

๐Ÿ”—opaque
Float.mul : Float โ†’ Float โ†’ Float
Float.mul : Float โ†’ Float โ†’ Float

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

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

๐Ÿ”—opaque
Float32.mul : Float32 โ†’ Float32 โ†’ Float32
Float32.mul : 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.

๐Ÿ”—opaque
Float.div : Float โ†’ Float โ†’ Float
Float.div : Float โ†’ Float โ†’ Float

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

In Lean, division by zero typically yields zero. For Float, it instead yields either Inf, -Inf, or NaN.

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

๐Ÿ”—opaque
Float32.div : Float32 โ†’ Float32 โ†’ Float32
Float32.div : 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.

๐Ÿ”—opaque
Float.pow : Float โ†’ Float โ†’ Float
Float.pow : Float โ†’ Float โ†’ Float

Raises one floating-point number to the power of another. Typically used via the ^ operator.

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

๐Ÿ”—opaque
Float32.pow : Float32 โ†’ Float32 โ†’ Float32
Float32.pow : Float32 โ†’ 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.

๐Ÿ”—opaque
Float.exp (x : Float) : Float
Float.exp (x : Float) : Float

Computes the exponential e^x of a floating-point number.

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

๐Ÿ”—opaque
Float32.exp : Float32 โ†’ Float32
Float32.exp : 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.

๐Ÿ”—opaque
Float.exp2 (x : Float) : Float
Float.exp2 (x : Float) : Float

Computes the base-2 exponential 2^x of a floating-point number.

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

๐Ÿ”—opaque
Float32.exp2 : Float32 โ†’ Float32
Float32.exp2 : 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.

20.6.2.5.1.ย ๆ นๆบ๐Ÿ”—

่ฎก็ฎ—่ดŸๆ•ฐ็š„ๅนณๆ–นๆ นๅพ—ๅˆฐ NaNใ€‚

๐Ÿ”—opaque
Float.sqrt : Float โ†’ Float
Float.sqrt : Float โ†’ Float

Computes the square root of a floating-point number.

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

๐Ÿ”—opaque
Float32.sqrt : Float32 โ†’ Float32
Float32.sqrt : 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.

๐Ÿ”—opaque
Float.cbrt : Float โ†’ Float
Float.cbrt : Float โ†’ Float

Computes the cube root of a floating-point number.

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

๐Ÿ”—opaque
Float32.cbrt : Float32 โ†’ Float32
Float32.cbrt : 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.

20.6.2.6.ย ๅฏนๆ•ฐ๐Ÿ”—

๐Ÿ”—opaque
Float.log (x : Float) : Float
Float.log (x : Float) : Float

Computes the natural logarithm ln x of a floating-point number.

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

๐Ÿ”—opaque
Float32.log : Float32 โ†’ Float32
Float32.log : 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.

๐Ÿ”—opaque
Float.log10 : Float โ†’ Float
Float.log10 : Float โ†’ Float

Computes the base-10 logarithm of a floating-point number.

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

๐Ÿ”—opaque
Float32.log10 : Float32 โ†’ Float32
Float32.log10 : 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.

๐Ÿ”—opaque
Float.log2 : Float โ†’ Float
Float.log2 : Float โ†’ Float

Computes the base-2 logarithm of a floating-point number.

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

๐Ÿ”—opaque
Float32.log2 : Float32 โ†’ Float32
Float32.log2 : 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.

20.6.2.7.ย ็ผฉๆ”พ๐Ÿ”—

๐Ÿ”—opaque
Float.scaleB (x : Float) (i : Int) : Float
Float.scaleB (x : Float) (i : Int) : Float

Efficiently computes x * 2^i.

This function does not reduce in the kernel.

๐Ÿ”—opaque
Float32.scaleB (x : Float32) (i : Int) : Float32
Float32.scaleB (x : Float32) (i : Int) :
  Float32

Efficiently computes x * 2^i.

This function does not reduce in the kernel.

20.6.2.8.ย ๅ››่ˆไบ”ๅ…ฅ๐Ÿ”—

๐Ÿ”—opaque
Float.round : Float โ†’ Float
Float.round : Float โ†’ Float

Rounds to the nearest integer, rounding away from zero at half-way points.

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

๐Ÿ”—opaque
Float32.round : Float32 โ†’ Float32
Float32.round : 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.

๐Ÿ”—opaque
Float.floor : Float โ†’ Float
Float.floor : Float โ†’ Float

Computes the floor of a floating-point number, which is the largest integer that's no larger than the given number.

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

Examples:

๐Ÿ”—opaque
Float32.floor : Float32 โ†’ Float32
Float32.floor : 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:

๐Ÿ”—opaque
Float.ceil : Float โ†’ Float
Float.ceil : Float โ†’ Float

Computes the ceiling of a floating-point number, which is the smallest integer that's no smaller than the given number.

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

Examples:

๐Ÿ”—opaque
Float32.ceil : Float32 โ†’ Float32
Float32.ceil : 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:

20.6.2.9.ย ไธ‰่ง’ๅญฆ๐Ÿ”—

20.6.2.9.1.ย ๆญฃๅผฆ๐Ÿ”—

๐Ÿ”—opaque
Float.sin : Float โ†’ Float
Float.sin : Float โ†’ Float

Computes the sine of a floating-point number in radians.

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

๐Ÿ”—opaque
Float32.sin : Float32 โ†’ Float32
Float32.sin : Float32 โ†’ 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.

๐Ÿ”—opaque
Float.sinh : Float โ†’ Float
Float.sinh : Float โ†’ Float

Computes the hyperbolic sine of a floating-point number.

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

๐Ÿ”—opaque
Float32.sinh : Float32 โ†’ Float32
Float32.sinh : 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.

๐Ÿ”—opaque
Float.asin : Float โ†’ Float
Float.asin : Float โ†’ Float

Computes the arc sine (inverse sine) of a floating-point number in radians.

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

๐Ÿ”—opaque
Float32.asin : Float32 โ†’ Float32
Float32.asin : 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.

๐Ÿ”—opaque
Float.asinh : Float โ†’ Float
Float.asinh : Float โ†’ Float

Computes the hyperbolic arc sine (inverse sine) of a floating-point number.

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

๐Ÿ”—opaque
Float32.asinh : Float32 โ†’ Float32
Float32.asinh : 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.

20.6.2.9.2.ย ไฝ™ๅผฆ๐Ÿ”—

๐Ÿ”—opaque
Float.cos : Float โ†’ Float
Float.cos : Float โ†’ Float

Computes the cosine of a floating-point number in radians.

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

๐Ÿ”—opaque
Float32.cos : Float32 โ†’ Float32
Float32.cos : 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.

๐Ÿ”—opaque
Float.cosh : Float โ†’ Float
Float.cosh : Float โ†’ Float

Computes the hyperbolic cosine of a floating-point number.

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

๐Ÿ”—opaque
Float32.cosh : Float32 โ†’ Float32
Float32.cosh : 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.

๐Ÿ”—opaque
Float.acos : Float โ†’ Float
Float.acos : Float โ†’ Float

Computes the arc cosine (inverse cosine) of a floating-point number in radians.

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

๐Ÿ”—opaque
Float32.acos : Float32 โ†’ Float32
Float32.acos : 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.

๐Ÿ”—opaque
Float.acosh : Float โ†’ Float
Float.acosh : Float โ†’ Float

Computes the hyperbolic arc cosine (inverse cosine) of a floating-point number.

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

๐Ÿ”—opaque
Float32.acosh : Float32 โ†’ Float32
Float32.acosh : 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.

20.6.2.9.3.ย ๅˆ‡็บฟ๐Ÿ”—

๐Ÿ”—opaque
Float.tan : Float โ†’ Float
Float.tan : Float โ†’ Float

Computes the tangent of a floating-point number in radians.

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

๐Ÿ”—opaque
Float32.tan : Float32 โ†’ Float32
Float32.tan : 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.

๐Ÿ”—opaque
Float.tanh : Float โ†’ Float
Float.tanh : Float โ†’ Float

Computes the hyperbolic tangent of a floating-point number.

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

๐Ÿ”—opaque
Float32.tanh : Float32 โ†’ Float32
Float32.tanh : 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.

๐Ÿ”—opaque
Float.atan : Float โ†’ Float
Float.atan : Float โ†’ Float

Computes the arc tangent (inverse tangent) of a floating-point number in radians.

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

๐Ÿ”—opaque
Float32.atan : Float32 โ†’ Float32
Float32.atan : 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.

๐Ÿ”—opaque
Float.atanh : Float โ†’ Float
Float.atanh : Float โ†’ Float

Computes the hyperbolic arc tangent (inverse tangent) of a floating-point number.

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

๐Ÿ”—opaque
Float32.atanh : Float32 โ†’ Float32
Float32.atanh : 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.

๐Ÿ”—opaque
Float.atan2 (y x : Float) : Float
Float.atan2 (y x : Float) : Float

Computes the arc tangent (inverse tangent) of y / x in radians, in the range -ฯ€โ€“ฯ€. The signs of the arguments determine the quadrant of the result.

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

๐Ÿ”—opaque
Float32.atan2 : Float32 โ†’ Float32 โ†’ Float32
Float32.atan2 :
  Float32 โ†’ 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.

20.6.2.10.ย ่ดŸๆ•ฐๅ’Œ็ปๅฏนๅ€ผ๐Ÿ”—

๐Ÿ”—opaque
Float.abs : Float โ†’ Float
Float.abs : Float โ†’ Float

Computes the absolute value of a floating-point number.

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

๐Ÿ”—opaque
Float32.abs : Float32 โ†’ Float32
Float32.abs : 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.

๐Ÿ”—opaque
Float.neg : Float โ†’ Float
Float.neg : Float โ†’ Float

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

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

๐Ÿ”—opaque
Float32.neg : Float32 โ†’ Float32
Float32.neg : 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.