TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.DecimalInterchange.Rounding.Runtime

Exact rounding on a decimal coefficient grid #

IEEE 754-2019 §4.3 requires five rounding directions for decimal arithmetic. The integer decision below works on an exact rational magnitude. In particular, midpoints are compared exactly; no binary floating approximation is used. Format precision, exponent range, and cohort selection are handled separately.

source
inductive FloatLib.Floats.Formats.DecimalInterchange.RoundingMode :
Type

The five IEEE 754-2019 §4.3 decimal rounding-direction attributes.

Instances For
    source
    @[instance_reducible]
    instance FloatLib.Floats.Formats.DecimalInterchange.instDecidableEqRoundingMode :
    DecidableEq RoundingMode
    source
    def FloatLib.Floats.Formats.DecimalInterchange.instReprRoundingMode.repr :
    RoundingMode → ℕ → Std.Format
    Instances For
      source
      @[instance_reducible]
      instance FloatLib.Floats.Formats.DecimalInterchange.instReprRoundingMode :
      Repr RoundingMode
      source
      @[instance_reducible]
      instance FloatLib.Floats.Formats.DecimalInterchange.instInhabitedRoundingMode :
      Inhabited RoundingMode
      source
      def FloatLib.Floats.Formats.DecimalInterchange.RoundingMode.increment (mode : RoundingMode) (negative : Bool) (lower : ℕ) (remainder : ℚ) :
      Bool

      Whether an inexact result should increase in magnitude at a given integer grid point. remainder is the exact fractional part, between zero and one.

      Instances For
        source
        def FloatLib.Floats.Formats.DecimalInterchange.RoundingMode.roundMagnitude (mode : RoundingMode) (negative : Bool) (x : ℚ) :
        ℕ

        Round a nonnegative exact rational magnitude to an integer coefficient. The sign affects the directed modes, including rounding a negative value to zero.

        Instances For
          source
          def FloatLib.Floats.Formats.DecimalInterchange.RoundingMode.roundSigned (mode : RoundingMode) (negative : Bool) (x : ℚ) :
          ℚ

          Apply the sign after rounding; callers retain the separate sign for signed zero.

          Instances For
            source
            def FloatLib.Floats.Formats.DecimalInterchange.RoundingMode.roundAt (mode : RoundingMode) (negative : Bool) (x : ℚ) (q : ℤ) :
            ℕ

            Rounding on a decimal grid whose quantum is 10 ^ q.

            Instances For