TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.DecimalInterchange.Formatting.Precision

Selecting decimal output precision #

IEEE 754 §5.12.2 distinguishes preserving the source quantum from requesting a number of significant digits, and Precision names that choice. Requested precision has no format-width cap: the coefficient is rounded once on the requested decimal grid, and extra requested digits are supplied by exact zeros. The text exponent is an unbounded integer, so output has no exponent overflow.

Zero at precision p is written with quantum 1-p. Special values keep their spellings and fields. Only inexact can be raised during finite output.

source
@[reducible, inline]
abbrev FloatLib.Floats.Formats.DecimalInterchange.Formatting.Precision :
Type

Output precision: keep the source quantum or request a significant-digit count.

Instances For
    source
    @[reducible, inline]
    abbrev FloatLib.Floats.Formats.DecimalInterchange.Formatting.significantDecimal (mode : RoundingMode) (value : Numerics.DecimalText.Decimal) (digits : ℕ+) :
    Numerics.DecimalText.Decimal

    Correctly rounded significant-digit output, with an unbounded requested precision.

    Instances For
      source
      structure FloatLib.Floats.Formats.DecimalInterchange.Formatting.TextOutcome :
      Type

      The external string together with the conversion's IEEE status flags.

      • text : String

        The generated external decimal character sequence.

      • status : Numerics.IEEEStatus

        Exceptions raised by this conversion. Output rounding can raise only inexact.

      Instances For
        source
        def FloatLib.Floats.Formats.DecimalInterchange.Formatting.instDecidableEqTextOutcome.decEq (x✝ x✝¹ : TextOutcome) :
        Decidable (x✝ = x✝¹)
        Instances For
          source
          @[instance_reducible]
          instance FloatLib.Floats.Formats.DecimalInterchange.Formatting.instDecidableEqTextOutcome :
          DecidableEq TextOutcome
          source
          def FloatLib.Floats.Formats.DecimalInterchange.Formatting.instReprTextOutcome.repr :
          TextOutcome → ℕ → Std.Format
          Instances For
            source
            @[instance_reducible]
            instance FloatLib.Floats.Formats.DecimalInterchange.Formatting.instReprTextOutcome :
            Repr TextOutcome
            source
            def FloatLib.Floats.Formats.DecimalInterchange.Formatting.format (mode : RoundingMode) (precision : Precision) (value : Datum) :
            TextOutcome

            Format a datum either exactly or to a requested significant-digit count. The inexact flag records a change of value, not a change of quantum.

            Instances For