TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.DecimalInterchange.Projection.Scale

Selecting the decimal rounding grid #

Count digits after scaling to the least quantum. This permits exact rational inputs, including values below the least subnormal. Nat.log computes the digit count from the scaled integer part. The selected exponent is unbounded above so overflow can be tested after precision rounding, as required by IEEE 754-2019 §7.4.

source
def FloatLib.Floats.Formats.DecimalInterchange.scaleShift (precision : ℕ) (scaled : ℚ) :
ℕ

Number of decimal places to remove from the least-quantum grid.

Instances For
    source
    def FloatLib.Floats.Formats.DecimalInterchange.roundingQuantum (f : Format) (magnitude : ℚ) :
    ℤ

    Least quantum retaining the format's precision, before overflow is handled. Zero selects the least quantum without constructing its radix power.

    Instances For