Decimal integral rounding

IEEE 754-2019 §§5.3.1 and 5.4.1 use the preferred quantum max(Q(x), 0). Rounding to the integer grid never increases a valid finite coefficient. If the preferred quantum is representable, the result fits without additional precision rounding. A custom layout whose maximum quantum is negative cannot store this preferred quantum; this binding returns invalid through quantizeMagnitude. Both APIs preserve the sign of a successful zero result; the exact variant signals numerical inexactness.

def FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.roundToIntegralExact (f : Format) (mode : RoundingMode) : Datum → Outcome

Round to an integral decimal value in the supplied rounding direction, signaling inexact. The mode argument represents the current rounding-direction attribute. An unrepresentable preferred quantum produces invalid, including on custom layouts.

def FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.roundToIntegral (f : Format) (mode : RoundingMode) (x : Datum) : Outcome

Integral rounding with an explicit direction, without signaling inexact.

@[reducible, inline]

abbrev FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.roundToIntegralTiesToEven (f : Format) (x : Datum) : Outcome

Round to the nearest integral value, choosing the even integer at a tie.

@[reducible, inline]

abbrev FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.roundToIntegralTiesToAway (f : Format) (x : Datum) : Outcome

Round to the nearest integral value, choosing away from zero at a tie.

@[reducible, inline]

abbrev FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.roundToIntegralTowardZero (f : Format) (x : Datum) : Outcome

Round to an integral value toward zero, without signaling inexact.

@[reducible, inline]

abbrev FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.roundToIntegralTowardPositive (f : Format) (x : Datum) : Outcome

Round to an integral value toward positive infinity, without signaling inexact.

@[reducible, inline]

abbrev FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.roundToIntegralTowardNegative (f : Format) (x : Datum) : Outcome

Round to an integral value toward negative infinity, without signaling inexact.