Binary external character output

format value writes a decimal that reads back as value, normally the shortest one or the exact value when that is short, and toString, repr and #eval show the same text. The style option selects every other output: exact decimal and hexadecimal digits, a count of significant digits, and fixed or scientific notation with a count of places. Styles that round do so once, in the mode option, and (status := true) returns the text with the inexact indicator of that rounding. Exponents are unbounded, so output cannot overflow or underflow.

The display writes inf, -inf and nan. The other styles keep the complete spellings of infinities and NaNs, including the sign, signaling state and payload of a NaN.

inductive FloatLib.Floats.Formats.BinaryInterchange.Model.TextStyle : Type

How format writes a binary value.

• shortest : TextStyle

  The shortest decimal that reads back as the value, or a short exact value: the display.

• exact : TextStyle

  Every digit of the exact decimal value, as a significand and a decimal exponent.

• significant (digits : ℕ+) : TextStyle

  This many significant decimal digits, as a significand and a decimal exponent.

• fixed (places : ℕ) : TextStyle

  Ordinary decimal notation with exactly this many digits after the point.

• scientific (places : ℕ) : TextStyle

  One digit before the point, this many after it, and an e exponent.

• hex (precision : Numerics.DecimalText.Precision := Numerics.DecimalText.Precision.exact) : TextStyle

  A hexadecimal significand with a p binary exponent, exact or to significant digits.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Internal.Status.formatFinite {fmt : FloatFormat} (style : TextStyle) (mode : IEEERoundingMode) (value : Model fmt) (exact : Numerics.Dyadic) : TextOutcome

Text of the finite value value, with exact value exact, in style, and its status.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Internal.Status.format {fmt : FloatFormat} (value : Model fmt) (style : TextStyle) (mode : IEEERoundingMode) : TextOutcome

Text of value in style with the inexact indicator of its rounding in mode.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.format {fmt : FloatFormat} (value : Model fmt) (style : TextStyle := TextStyle.shortest) (mode : IEEERoundingMode := IEEERoundingMode.nearest) (status : Bool := false) : match status with | true => TextOutcome | false => String

Write a value of any binary descriptor as text.

By default this is the display: the exact value when it has at most d significant digits (d is 17 for binary64), and otherwise the shortest decimal the search finds that parse reads back as value, with the exact value as the fallback. It uses fixed notation from 0.0001 up to 10^d and an e exponent otherwise. toString, repr and #eval use it. style selects the exact decimal or hexadecimal digits, significant digits, or fixed or scientific notation. Styles that round do so once in mode, and with mode the display reads back in that mode. With status := true the result also carries the inexact indicator of that rounding.

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.instToString {fmt : FloatFormat} : ToString (Model fmt)

Values print as a decimal that reads back as the same value, normally the shortest.

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.instRepr {fmt : FloatFormat} : Repr (Model fmt)

#eval and repr show the same decimal, parenthesized when negative inside an argument.

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.instReprIEEEOutcome {fmt : FloatFormat} : Repr (IEEEOutcome fmt)

#eval shows the three fields, displaying the value as toString does.