Decimal rational arithmetic

Addition, subtraction, multiplication, division, and fused multiply-add compute their finite intermediate values in ℚ, then project once. Preferred exponents follow IEEE 754-2019 §5.4.1; signs and exceptional operands follow §§6–7.

NaN propagation chooses the first NaN operand, preserving its sign and payload when the payload fits the destination. Any signaling operand raises invalid. For fma(0, infinity, quietNaN), this implementation raises invalid, one of the two behaviors permitted by §7.2(c). These operations return default exception flags; they do not implement trapping or a mutable floating-point environment.

def FloatLib.Floats.Formats.DecimalInterchange.Datum.finiteValue (negative : Bool) (coefficient : ℕ) (quantum : ℤ) : ℚ

Exact value of a finite representation, including either signed zero.

def FloatLib.Floats.Formats.DecimalInterchange.Datum.isSignaling : Datum → Bool

Test the signaling bit only on a NaN.

def FloatLib.Floats.Formats.DecimalInterchange.Datum.negate : Datum → Datum

Reverse the sign bit without quieting a NaN or changing its payload.

def FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.nanResult (f : Format) (negative : Bool) (payload : ℕ) (invalid : Bool) : Outcome

Quiet NaN propagation. An unrepresentable payload becomes zero.

def FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.invalidResult : Outcome

Default result of an invalid operation without an input NaN.

def FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.zeroSumSign (mode : RoundingMode) (left right : Bool) : Bool

Sign of an exact zero sum. Equal signs survive; cancellation rounds downward to -0.

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

Addition, with preferred quantum the smaller operand quantum.

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

Subtraction preserves input NaN diagnostics before reversing the second numeric sign.

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

Multiplication, with preferred quantum the sum of the operand quanta.

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

Division, including the distinction between finite nonzero/zero and infinity/zero. By §5.2, an infinity has quantum exponent +∞; finite/infinity therefore selects the smallest quantum in the signed-zero cohort.

def FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.addInfinity (f : Format) (negative : Bool) : Datum → Outcome

Add a signed infinity to a third operand after a fused product is classified.

def FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.invalidProduct : Datum → Datum → Bool

Test the invalid zero-times-infinity product, without assigning a value to it.

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

Fused multiply-add with unbounded intermediate range and exactly one rounding. Neither an overflowing nor an underflowing intermediate product raises a flag.