TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.BinaryInterchange.Conversion.Text.Digits

Exact and significant-digit text of binary values #

Exact decimal and hexadecimal output preserve every finite value. Requested precision is an arbitrary positive digit count. Both radices use the shared digit-grid and carry calculation. Exponents are unbounded integers, so output can raise inexact but cannot overflow or underflow. Model.format selects these digits through its style option.

source
inductive FloatLib.Floats.Formats.BinaryInterchange.Model.TextRadix :
Type

Radix of the external significand. Hexadecimal output writes its binary exponent in decimal.

  • decimal : TextRadix

    Decimal digits and an optional e exponent.

  • hexadecimal : TextRadix

    Hexadecimal digits with a 0x prefix and mandatory p exponent.

Instances For
    source
    @[instance_reducible]
    instance FloatLib.Floats.Formats.BinaryInterchange.Model.instDecidableEqTextRadix :
    DecidableEq TextRadix
    source
    @[instance_reducible]
    instance FloatLib.Floats.Formats.BinaryInterchange.Model.instReprTextRadix :
    Repr TextRadix
    source
    def FloatLib.Floats.Formats.BinaryInterchange.Model.instReprTextRadix.repr :
    TextRadix → ℕ → Std.Format
    Instances For
      source
      structure FloatLib.Floats.Formats.BinaryInterchange.Model.TextOutcome :
      Type

      A generated external character sequence and the exceptions raised while producing it.

      • text : String

        Decimal, hexadecimal, infinity or diagnostic NaN text.

      • status : Numerics.IEEEStatus

        Output rounding can raise inexact, and every other exception indicator stays clear.

      Instances For
        source
        @[instance_reducible]
        instance FloatLib.Floats.Formats.BinaryInterchange.Model.instDecidableEqTextOutcome :
        DecidableEq TextOutcome
        source
        def FloatLib.Floats.Formats.BinaryInterchange.Model.instDecidableEqTextOutcome.decEq (x✝ x✝¹ : TextOutcome) :
        Decidable (x✝ = x✝¹)
        Instances For
          source
          def FloatLib.Floats.Formats.BinaryInterchange.Model.instReprTextOutcome.repr :
          TextOutcome → ℕ → Std.Format
          Instances For
            source
            @[instance_reducible]
            instance FloatLib.Floats.Formats.BinaryInterchange.Model.instReprTextOutcome :
            Repr TextOutcome
            source
            def FloatLib.Floats.Formats.BinaryInterchange.Model.roundTextMagnitude (mode : IEEERoundingMode) (negative : Bool) (x : ℚ) :
            ℕ

            Integer magnitude rounding for an external digit grid, using the exact integer rounders.

            The magnitude x is nonnegative. Nearest-away rounding is Numerics.roundQuotient .nearestAway on its numerator and denominator, and rounding away from zero is the ceiling.

            Instances For
              source
              @[inline]
              def FloatLib.Floats.Formats.BinaryInterchange.Model.formatDyadicText (mode : IEEERoundingMode) (radix : TextRadix) (precision : Numerics.DecimalText.Precision) (value : Numerics.Dyadic) :
              TextOutcome

              Exact or significant-digit output for an unrounded dyadic, with numerical inexactness.

              Instances For