def Float32.radix : Nat

Equations

• Float32.radix = 2

def Float32.digits : Nat

Equations

• Float32.digits = 24

def Float32.minExp : Int

Equations

• Float32.minExp = -125

def Float32.maxExp : Nat

Equations

• Float32.maxExp = 128

def Float32.exponent (x : Float32) : Int

Equations

• x.exponent = x.frExp.snd

def Float32.significand (x : Float32) : Float32

Equations

• x.significand = x.frExp.fst

def Float32.scale (i : Int) (x : Float32) : Float32

Equations

• Float32.scale i x = x.scaleB i

def Float32.decode (x : Float32) : Int × Int

Equations

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

def Float32.encode : Int × Int → Float32

Equations

• Float32.encode (m, e) = (if m < 0 then Float32.neg else id) (Float32.ofBinaryScientific m.natAbs e)

def Float32.properFraction {b : Type u} [Printf.Integral b] (x : Float32) : b × Float32

Equations

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

def Float32.truncate {b : Type u} [Printf.Integral b] (x : Float32) : b

Equations

• x.truncate = x.properFraction.fst

def Float32.isNegativeZero (x : Float32) : Bool

Equations

• x.isNegativeZero = decide (x.toBits = (-0.0).toBits)

def Float.radix : Nat

Equations

• Float.radix = 2

def Float.digits : Nat

Equations

• Float.digits = 53

def Float.minExp : Int

Equations

• Float.minExp = -1021

def Float.maxExp : Nat

Equations

• Float.maxExp = 1024

def Float.significand (x : Float) : Float

Equations

• x.significand = x.frExp.fst

def Float.exponent (x : Float) : Int

Equations

• x.exponent = x.frExp.snd

def Float.scale (i : Int) (x : Float) : Float

Equations

• Float.scale i x = x.scaleB i

def Float.decode (x : Float) : Int × Int

Equations

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

def Float.encode : Int × Int → Float

Equations

• Float.encode (m, e) = (if m < 0 then Float.neg else id) (Float.ofBinaryScientific m.natAbs e)

def Float.properFraction {b : Type u} [Printf.Integral b] (x : Float) : b × Float

Equations

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

def Float.truncate {b : Type u} [Printf.Integral b] (x : Float) : b

Equations

• x.truncate = x.properFraction.fst

def Float.isNegativeZero (x : Float) : Bool

Equations

• x.isNegativeZero = decide (x.toBits = (-0.0).toBits)

class Printf.Real (a : Type u) extends Printf.OfInt a, Printf.Num a, Neg a, Ord a, LT a, BEq a : Type u

• ofInt : Int → a
• add : a → a → a
• sub : a → a → a
• mul : a → a → a
• div : a → a → a
• compare : a → a → Ordering
• lt : a → a → Prop
• le : a → a → Prop
• beq : a → a → Bool
• neg : a → a

instance Printf.instRealFloat32 : Real Float32

Equations

• Printf.instRealFloat32 = { toOfInt := Printf.instOfIntFloat32, toNum := Printf.instNumFloat32, toNeg := instNegFloat32 }

instance Printf.instRealFloat : Real Float

Equations

• Printf.instRealFloat = { toOfInt := Printf.instOfIntFloat, toNum := Printf.instNumFloat, toNeg := instNegFloat }

class Printf.Fractional (a : Type u) extends Printf.Num a, Printf.OfInt a : Type u

• add : a → a → a
• sub : a → a → a
• mul : a → a → a
• div : a → a → a
• compare : a → a → Ordering
• lt : a → a → Prop
• le : a → a → Prop
• beq : a → a → Bool
• ofInt : Int → a
• recip : a → a

  Reciprocal fraction

instance Printf.instFractionalFloat32 : Fractional Float32

Equations

• Printf.instFractionalFloat32 = { toNum := Printf.instNumFloat32, toOfInt := Printf.instOfIntFloat32, recip := fun (x : Float32) => 1 / x }

instance Printf.instFractionalFloat : Fractional Float

Equations

• Printf.instFractionalFloat = { toNum := Printf.instNumFloat, toOfInt := Printf.instOfIntFloat, recip := fun (x : Float) => 1 / x }

inductive Printf.FFFormat : Type

• Exponent : FFFormat
• Fixed : FFFormat
• Generic : FFFormat

instance Printf.instReprFFFormat : Repr FFFormat

Equations

• Printf.instReprFFFormat = { reprPrec := Printf.reprFFFormat✝ }

instance Printf.instDecidableEqFFFormat : DecidableEq FFFormat

Equations

• Printf.instDecidableEqFFFormat x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯

instance Printf.instBEqFFFormat : BEq FFFormat

Equations

• Printf.instBEqFFFormat = { beq := Printf.beqFFFormat✝ }

instance Printf.instInhabitedFFFormat : Inhabited FFFormat

Equations

• Printf.instInhabitedFFFormat = { default := Printf.FFFormat.Exponent }

instance Printf.instNonemptyFFFormat : Nonempty FFFormat

instance Printf.instTypeNameFFFormat : TypeName FFFormat

Equations

• Printf.instTypeNameFFFormat = Printf.inst✝

class Printf.RealFrac (a : Type u) extends Printf.Real a, Printf.Fractional a : Type (max (u + 1) (v + 1))

• ofInt : Int → a
• add : a → a → a
• sub : a → a → a
• mul : a → a → a
• div : a → a → a
• compare : a → a → Ordering
• lt : a → a → Prop
• le : a → a → Prop
• beq : a → a → Bool
• neg : a → a
• recip : a → a
• properFraction {b : Type u} [Integral b] : a → b × a
• truncate {b : Type v} [Integral b] : a → b

  truncate x returns the integer nearest x between zero and x

• round {b : Type v} [Integral b] : a → b
• ceil {b : Type v} [Integral b] : a → b
• floor {b : Type v} [Integral b] : a → b

instance Printf.instRealFracFloat32 : RealFrac Float32

Equations

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

instance Printf.instRealFracFloat : RealFrac Float

Equations

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

class Printf.Floating (a : Type u) extends Printf.Fractional a, OfScientific a : Type u

• add : a → a → a
• sub : a → a → a
• mul : a → a → a
• div : a → a → a
• compare : a → a → Ordering
• lt : a → a → Prop
• le : a → a → Prop
• beq : a → a → Bool
• ofInt : Int → a
• recip : a → a
• ofScientific (mantissa : Nat) (exponentSign : Bool) (decimalExponent : Nat) : a
• pi : a
• exp : a → a
• log : a → a

  Natural Logarithm

• sqrt : a → a
• sin : a → a
• cos : a → a
• tan : a → a
• asin : a → a
• acos : a → a
• atan : a → a
• sinh : a → a
• cosh : a → a
• tanh : a → a
• asinh : a → a
• acosh : a → a
• atanh : a → a

def Printf.Floating.logBase {f : Type u} [Floating f] (base x : f) : f

Equations

• Printf.Floating.logBase base x = Printf.Floating.log x / Printf.Floating.log base

instance Printf.instFloatingFloat32 : Floating Float32

Equations

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

instance Printf.instFloatingFloat : Floating Float

Equations

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

class Printf.RealFloat (a : Type u) extends Printf.RealFrac a, Printf.Floating a, Repr a, ToString a : Type (max (u + 1) (u_1 + 1))

• ofInt : Int → a
• add : a → a → a
• sub : a → a → a
• mul : a → a → a
• div : a → a → a
• compare : a → a → Ordering
• lt : a → a → Prop
• le : a → a → Prop
• beq : a → a → Bool
• neg : a → a
• recip : a → a
• properFraction {b : Type u} [Integral b] : a → b × a
• truncate {b : Type u_1} [Integral b] : a → b
• round {b : Type u_1} [Integral b] : a → b
• ceil {b : Type u_1} [Integral b] : a → b
• floor {b : Type u_1} [Integral b] : a → b
• ofScientific (mantissa : Nat) (exponentSign : Bool) (decimalExponent : Nat) : a
• pi : a
• exp : a → a
• log : a → a
• sqrt : a → a
• sin : a → a
• cos : a → a
• tan : a → a
• asin : a → a
• acos : a → a
• atan : a → a
• sinh : a → a
• cosh : a → a
• tanh : a → a
• asinh : a → a
• acosh : a → a
• atanh : a → a
• reprPrec : a → Nat → Std.Format
• toString : a → String
• radix : Nat

  The radix of the representation (often 2)

• digits : Nat

  The number of digits of 'radix' in the significand

• range : Int × Int

  The lowest and highest values the exponent may assume

• decode : a → Int × Int

  The function decodeFloat applied to a real floating-point number returns the significand expressed as an Integer and an appropriately scaled exponent (an Int). If decodeFloat x yields (m,n), then x is equal in value to m*b^n, where b is the floating-point radix, and furthermore, either m and n are both zero or else b^(d-1) <= abs m < b^d, where d is the value of RealFloat.digits x. In particular, decodeFloat 0 = (0,0). If the type contains a negative zero, also decodeFloat (-0.0) = (0,0) NOTE: The result of decodeFloat x is unspecified if either of isNaN x or isInfinite x is True.

• encode : Int × Int → a

  encodeFloat performs the inverse of decodeFloat in the sense that for finite x with the exception of -0.0, uncurry encodeFloat (decodeFloat x) = x. encodeFloat m n is one of the two closest representable floating-point numbers to m*b^n (or ±Infinity if overflow occurs); usually the closer, but if m contains too many bits, the result may be rounded in the wrong direction.

• exponent : a → Int
• significand : a → a
• scale : Int → a → a
• isNaN : a → Bool
• isInfinite : a → Bool
• isFinite : a → Bool
• isNegative : a → Bool
• isNegativeZero : a → Bool
• isIEEE : Bool

def Printf.clamp : Int → Int → Int

Equations

• Printf.clamp x✝¹ x✝ = max (-x✝¹) (min x✝¹ x✝)

instance Printf.instRealFloatFloat32 : RealFloat Float32

Equations

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

instance Printf.instRealFloatFloat : RealFloat Float

Equations

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

@[inline]

def Printf.expt {b e p : Type u} [HPow b e p] (base : b) (n : e) : p

Equations

• Printf.expt base n = base ^ n

def Printf.RealFloat.toDigits {a : Type u} [RealFloat a] (base : Nat) (x : a) : List Int × Int

Based on "Printing Floating-Point Numbers Quickly and Accurately" by R.G. Burger and R.K. Dybvig in PLDI 96. This version uses a much slower logarithm estimator. It should be improved.

'floatToDigits' takes a base and a non-negative 'RealFloat' number, and returns a list of digits and an exponent.

In particular, if x >= 0, and floatToDigits base x = ([d1,d2,...,dn], e), then (1) @n >= 1@

(2) @x = 0.d1d2...dn * (base**e)@

(3) @0 <= di <= base-1@

Equations

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

partial def Printf.RealFloat.toDigits.fixup (base : Nat) (r : Int) (s mUp : Nat) (n : Int) : Int

partial def Printf.RealFloat.toDigits.gen (base : Nat) (ds : List Int) (rn sN mUpN mDnN : Int) : List Int

def Printf.roundTo (base d : Int) (is : List Int) : Int × List Int

Equations

• Printf.roundTo base d is = match Printf.roundTo.go base (base / 2) d true is with | (0, xs) => (0, xs) | (1, xs) => (1, 1 :: xs) | x => panic "roundTo: bad value"

def Printf.roundTo.go (base b2 : Int) : Int → Bool → List Int → Int × List Int

Equations

• One or more equations did not get rendered due to their size.
• Printf.roundTo.go base b2 x✝¹ x✝ [] = (0, List.replicate x✝¹.toNat 0)
• Printf.roundTo.go base b2 0 x✝ (x_3 :: xs) = if (x_3 == b2 && x✝ && xs.all fun (x : Int) => x == 0) = true then (0, []) else (if x_3 ≥ b2 then 1 else 0, [])

@[reducible, inline]

abbrev Printf.ShowS : Type

Equations

• Printf.ShowS = (String → String)

def Printf.showString : String → ShowS

Equations

• Printf.showString = String.append

def Printf.RealFloat.format {f : Type u} [RealFloat f] (fmt : FFFormat) (dec? : Option Int) (self : f) (alt : Bool := false) : String

Equations

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

partial def Printf.RealFloat.format.doFmt (dec? : Option Int) (alt : Bool := false) (fmt : FFFormat) : List Int × Int → String

partial def Printf.RealFloat.format.doFmt.f : Nat → String → String → String

def Printf.RealFloat.format.base : Nat

Equations

• Printf.RealFloat.format.base = 10

def Printf.RealFloat.format.replicate (n : Nat) (c : Char) : String

Equations

• Printf.RealFloat.format.replicate n c = (List.replicate n c).asString

def Printf.RealFloat.format.reverse (s : String) : String

Equations

• Printf.RealFloat.format.reverse s = s.toList.reverse.asString

def Printf.RealFloat.format.splitAt (n : Nat) (s : String) : String × String

Equations

• Printf.RealFloat.format.splitAt n s = (s.take n, s.drop n)

def Printf.RealFloat.format.mk0 : String → String

Equations

• Printf.RealFloat.format.mk0 "" = "0"
• Printf.RealFloat.format.mk0 x✝ = x✝

def Printf.showEFloat {f : Type u} [RealFloat f] : Option Int → f → ShowS

Equations

• Printf.showEFloat = (fun (x : f → String) => Printf.showString ∘ x) ∘ fun (dec? : Option Int) (self : f) => Printf.RealFloat.format Printf.FFFormat.Exponent dec? self

def Printf.showFFloat {f : Type u} [RealFloat f] (alt : Bool := false) : Option Int → f → ShowS

Equations

• Printf.showFFloat alt = (fun (x : f → String) => Printf.showString ∘ x) ∘ fun (dec? : Option Int) (self : f) => Printf.RealFloat.format Printf.FFFormat.Fixed dec? self alt

def Printf.showGFloat {f : Type u} [RealFloat f] (alt : Bool := false) : Option Int → f → ShowS

Equations

• Printf.showGFloat alt = (fun (x : f → String) => Printf.showString ∘ x) ∘ fun (dec? : Option Int) (self : f) => Printf.RealFloat.format Printf.FFFormat.Generic dec? self alt