def Float.inf : Float

The floating point value "positive infinity", also used to represent numerical computations which produce finite values outside of the representable range of Float.

Equations

• Float.inf = 1 / 0

def Float.nan : Float

The floating point value "not a number", used to represent erroneous numerical computations such as 0 / 0. Using nan in any float operation will return nan, and all comparisons involving nan return false, including in particular nan == nan.

Equations

• Float.nan = 0 / 0

def Float.toRatParts (f : Float) : Option (Int × Int)

Returns v, exp integers such that f = v * 2^exp. (e is not minimal, but v.abs will be at most 2^53 - 1.) Returns none when f is not finite (i.e. inf, -inf or a nan).

Equations

• One or more equations did not get rendered due to their size.

def Float.toRatParts' (f : Float) : Option (Int × Int)

Returns v, exp integers such that f = v * 2^exp. Like toRatParts, but e is guaranteed to be minimal (n is always odd), unless n = 0. n.abs will be at most 2^53 - 1 because Float has 53 bits of precision. Returns none when f is not finite (i.e. inf, -inf or a nan).

Equations

• One or more equations did not get rendered due to their size.

partial def Float.toRatParts'.trailingZeros (v : UInt64) (c : UInt8) : UInt8

Calculates the number of trailing bits in a UInt64. Requires v ≠ 0.

def Float.toStringFull (f : Float) : String

Converts f to a string, including all decimal digits.

Equations

• One or more equations did not get rendered due to their size.

def Nat.divFloat (a : Nat) (b : Nat) : Float

Divide two natural numbers, to produce a correctly rounded (nearest-ties-to-even) Float result.

Equations

• One or more equations did not get rendered due to their size.

def Int.divFloat (a : Int) (b : Int) : Float

Divide two integers, to produce a correctly rounded (nearest-ties-to-even) Float result.

Equations

• a.divFloat b = if (decide (a ≥ 0) == decide (b ≥ 0)) = true then a.natAbs.divFloat b.natAbs else -a.natAbs.divFloat b.natAbs