Documentation

Batteries.Lean.Float

source
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
source
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
source
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.
source
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.
source
partial def Float.toRatParts'.trailingZeros (v : UInt64) (c : UInt8) :
UInt8

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

source
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.
source
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.
source
def Int.divFloat (a : Int) (b : Int) :
Float

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

Equations