Decimal exponent operations

scale implements IEEE 754-2019 §5.3.3 scaleB: multiply by an exact integral power of ten, then round once. Its preferred exponent is the input quantum plus the scale. The integer argument is unbounded, without the coefficient restriction of the older General Decimal Arithmetic scaleb operation.

decimalExponent implements logB with an integer result format. For zero, infinity and NaN §5.3.3 asks for a value outside the range ±2 × (emax + p - 1), where emax is the largest exponent of a finite value in scientific form. The sentinel is 2 × (emax + p - 1) + 1, enlarged if needed so that it also exceeds twice the absolute bound on every finite exponent, and zero gets its negation. Exceptional inputs raise invalid, including quiet NaNs, as specified for an integer logBFormat in §5.3.3. These are default exception results, without a mutable environment or alternate exception handling.

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

Multiply by 10^n and round once (IEEE 754 scaleB), using the input quantum plus n as the preferred quantum.

structure FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.DecimalExponentOutcome : Type

Integer result and default status for an exponent query.

• value : ℤ

  Radix exponent for a nonzero finite input, or the signed exceptional sentinel.

• status : Numerics.IEEEStatus

  Default exception flags. Exceptional integer results signal invalid.

@[instance_reducible]

instance FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.instDecidableEqDecimalExponentOutcome : DecidableEq DecimalExponentOutcome

def FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.instDecidableEqDecimalExponentOutcome.decEq (x✝ x✝¹ : DecimalExponentOutcome) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.instReprDecimalExponentOutcome : Repr DecimalExponentOutcome

def FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.instReprDecimalExponentOutcome.repr : DecimalExponentOutcome → ℕ → Std.Format

def FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.logBBound (f : Format) : ℤ

The IEEE 754-2019 §5.3.3 bound emax + p - 1 for an integer logB result. Here emax = maxQuantum + p - 1 is the largest scientific exponent of a finite value.

def FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.decimalExponentSentinel (f : Format) : ℤ

Exceptional integer exponent. It lies outside ±2 × (emax + p - 1) as §5.3.3 requires, and beyond twice either absolute finite exponent bound.

def FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.decimalExponent (f : Format) : Datum → DecimalExponentOutcome

Leading decimal exponent as an integer (IEEE 754 logB). Zero uses the negative sentinel; infinity and either kind of NaN use the positive one.