Fixed and scientific decimal output

Both notations take a number of digits after the decimal point. Fixed output rounds on the grid 10^(-places), and scientific output keeps places + 1 significant digits. Rounding happens once on the exact decimal value, before inserting the point and exponent. Trailing zeros express the requested precision, and a negative value that rounds to zero retains its sign.

These operations use exact integer arithmetic for any binary descriptor. They do not call the host floating-point printer. Model.format selects them with style := .fixed places and style := .scientific places.

def FloatLib.Floats.Formats.BinaryInterchange.Model.roundFixed (mode : IEEERoundingMode) (places : ℕ) (value : Numerics.DecimalText.Decimal) : Numerics.DecimalText.Decimal

Round an exact decimal once on the grid 10^(-places).

def FloatLib.Floats.Formats.BinaryInterchange.Model.roundScientific (mode : IEEERoundingMode) (places : ℕ) (value : Numerics.DecimalText.Decimal) : Numerics.DecimalText.Decimal

Round an exact decimal once to places + 1 significant digits.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.fixedText (mode : IEEERoundingMode) (places : ℕ) (value : Numerics.Dyadic) : TextOutcome

Fixed output of an exact dyadic with places fractional digits and its rounding status.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.scientificText (mode : IEEERoundingMode) (places : ℕ) (value : Numerics.Dyadic) : TextOutcome

Scientific output of an exact dyadic with places + 1 significant digits and its status.