TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.BinaryInterchange.Conversion.Text.DecimalFormatting

Fixed and scientific decimal output #

Both styles take a number of digits after the decimal point. Fixed output rounds on the grid 10^(-places); scientific output keeps places + 1 significant digits. Rounding happens once on the exact decimal value, before inserting the point and exponent. Trailing zeros express the requested precision, and a negative value that rounds to zero retains its sign.

These operations use exact integer arithmetic for any binary descriptor. They do not call the host floating-point printer. Infinities and NaNs use the same diagnostic spelling as formatDecimal.

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

Conventional decimal notation, with precision measured after the decimal point.

  • fixed (places : ℕ) : DecimalStyle

    Ordinary decimal notation with exactly this many fractional digits.

  • scientific (places : ℕ) : DecimalStyle

    One digit before the decimal point and this many after it, followed by an e exponent.

Instances For
    source
    @[instance_reducible]
    instance FloatLib.Floats.Formats.BinaryInterchange.Model.instDecidableEqDecimalStyle :
    DecidableEq DecimalStyle
    source
    def FloatLib.Floats.Formats.BinaryInterchange.Model.instDecidableEqDecimalStyle.decEq (x✝ x✝¹ : DecimalStyle) :
    Decidable (x✝ = x✝¹)
    Instances For
      source
      @[instance_reducible]
      instance FloatLib.Floats.Formats.BinaryInterchange.Model.instReprDecimalStyle :
      Repr DecimalStyle
      source
      def FloatLib.Floats.Formats.BinaryInterchange.Model.instReprDecimalStyle.repr :
      DecimalStyle → ℕ → Std.Format
      Instances For
        source
        def FloatLib.Floats.Formats.BinaryInterchange.Model.roundDecimalForStyle (mode : IEEERoundingMode) (style : DecimalStyle) (value : Numerics.DecimalText.Decimal) :
        Numerics.DecimalText.Decimal

        Round an exact decimal once at the precision required by the selected notation.

        Instances For
          source
          def FloatLib.Floats.Formats.BinaryInterchange.Model.renderDecimalStyle (style : DecimalStyle) (value : Numerics.DecimalText.Decimal) :
          String

          Render a decimal already rounded by roundDecimalForStyle with this same style. The decimal record supplies the fractional places; this step only inserts notation.

          Instances For
            source
            def FloatLib.Floats.Formats.BinaryInterchange.Model.formatDyadicDecimal (mode : IEEERoundingMode) (style : DecimalStyle) (value : Numerics.Dyadic) :
            TextOutcome

            Fixed or scientific output of an exact dyadic, including numerical rounding status.

            Instances For
              source
              def FloatLib.Floats.Formats.BinaryInterchange.Model.formatDecimalWithStatus {fmt : FloatFormat} (mode : IEEERoundingMode) (style : DecimalStyle) (value : Model fmt) :
              TextOutcome

              Decimal output with an explicit notation, rounding direction, and inexact indicator.

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

                Nearest-even decimal output with exactly places digits after the decimal point.

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

                  Nearest-even scientific output with places + 1 significant digits and an e exponent.

                  Instances For