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.