Selecting decimal output precision

IEEE 754 §5.12.2 distinguishes preserving the source quantum from requesting a number of significant digits. Precision makes this choice explicit. Requested precision has no format-width cap: the coefficient is rounded once on the requested decimal grid, and extra requested digits are supplied by exact zeros. The text exponent is an unbounded integer, so output has no exponent overflow.

Zero at precision p is written with quantum 1-p. Special values keep their exact spellings and fields. Only inexact can be raised during finite output.

@[reducible, inline]

abbrev FloatLib.Floats.Formats.DecimalInterchange.Formatting.Precision : Type

Preserving the original quantum and requesting a digit count are separate operations.

@[reducible, inline]

abbrev FloatLib.Floats.Formats.DecimalInterchange.Formatting.significantDecimal (mode : RoundingMode) (value : Numerics.DecimalText.Decimal) (digits : ℕ+) : Numerics.DecimalText.Decimal

Correctly rounded significant-digit output, with an unbounded requested precision.

structure FloatLib.Floats.Formats.DecimalInterchange.Formatting.TextOutcome : Type

The external string together with the conversion's IEEE status flags.

• text : String

  The generated external decimal character sequence.

• status : Status

  Exceptions raised by this conversion; output rounding can raise only inexact.

def FloatLib.Floats.Formats.DecimalInterchange.Formatting.instDecidableEqTextOutcome.decEq (x✝ x✝¹ : TextOutcome) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance FloatLib.Floats.Formats.DecimalInterchange.Formatting.instDecidableEqTextOutcome : DecidableEq TextOutcome

def FloatLib.Floats.Formats.DecimalInterchange.Formatting.instReprTextOutcome.repr : TextOutcome → ℕ → Std.Format

@[instance_reducible]

instance FloatLib.Floats.Formats.DecimalInterchange.Formatting.instReprTextOutcome : Repr TextOutcome

def FloatLib.Floats.Formats.DecimalInterchange.Formatting.format (mode : RoundingMode) (precision : Precision) (value : Datum) : TextOutcome

Format a datum either exactly or to a requested significant-digit count. The inexact flag records numerical rounding, rather than a change of quantum.