TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.BinaryInterchange.Conversion.Text.Formatting

Binary external character output #

Exact decimal and hexadecimal output preserve finite values, signed zeros, infinities and NaN diagnostics. 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. Signaling NaNs retain their signaling state without invalid.

External conversion is explicit through formatDecimal, formatHex, or formatWithStatus. The existing format and ToString retain the compact dyadic diagnostic display, which omits NaN metadata.

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

Radix of the external significand; hexadecimal output still has a decimal binary exponent.

  • 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
      @[reducible, inline]
      abbrev FloatLib.Floats.Formats.BinaryInterchange.Model.TextPrecision :
      Type

      Exact output or an arbitrary positive significant-digit count, shared with decimal formats.

      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; all other exception indicators remain 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 existing exact integer rounders.

              Instances For
                source
                def FloatLib.Floats.Formats.BinaryInterchange.Model.formatDyadicText (mode : IEEERoundingMode) (radix : TextRadix) (precision : TextPrecision) (value : Numerics.Dyadic) :
                TextOutcome

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

                Instances For
                  source
                  def FloatLib.Floats.Formats.BinaryInterchange.Model.formatWithStatus {fmt : FloatFormat} (mode : IEEERoundingMode) (radix : TextRadix) (precision : TextPrecision) (value : Model fmt) :
                  TextOutcome

                  Format any binary descriptor at exact or requested precision, preserving special metadata.

                  Instances For
                    source
                    def FloatLib.Floats.Formats.BinaryInterchange.Model.formatDecimal {fmt : FloatFormat} (value : Model fmt) :
                    String

                    Exact decimal external output, preserving signed zero and complete NaN metadata.

                    Instances For
                      source
                      def FloatLib.Floats.Formats.BinaryInterchange.Model.formatHex {fmt : FloatFormat} (value : Model fmt) :
                      String

                      Exact hexadecimal display, including the complete diagnostic spelling for a NaN.

                      Instances For
                        source
                        def FloatLib.Floats.Formats.BinaryInterchange.Model.format {fmt : FloatFormat} (value : Model fmt) :
                        String

                        Host-independent diagnostic display, using compact dyadic text for finite values. Use formatDecimal or formatHex for external conversion with NaN metadata.

                        Instances For
                          source
                          @[instance_reducible]
                          instance FloatLib.Floats.Formats.BinaryInterchange.Model.instToString {fmt : FloatFormat} :
                          ToString (Model fmt)