TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.Posit.Configured.Algebraic.RationalPower.Runtime

Configured once-rounded powers and exponentials #

These codec adapters forward to the exactly rounded model implementations of pow, exp2, exp10, and their fused minus-one forms. Carrier selection adds no rounding.

The model kernels decide equality with a rounding boundary exactly and separate the other cases with certified logarithm enclosures. They raise the base's root to the exponent's numerator only by exponentiation capped against the boundary, so large exponents create no large integers. Small integer exponents use exact rational arithmetic before the single final rounding.

source
@[inline]
def FloatLib.Floats.ExecFloat.Posit.pow {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (base exponent : ExecFloat (Formats.Posit.Configured.Family format code plan)) :
ExecFloat (Formats.Posit.Configured.Family format code plan)

Exactly rounded power. NaR propagates, zero requires a positive exponent, and negative bases require integral exponents.

Instances For
    source
    @[inline]
    def FloatLib.Floats.ExecFloat.Posit.exp2 {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) :
    ExecFloat (Formats.Posit.Configured.Family format code plan)

    Exactly rounded base-two exponential. NaR propagates.

    Instances For
      source
      @[inline]
      def FloatLib.Floats.ExecFloat.Posit.exp10 {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) :
      ExecFloat (Formats.Posit.Configured.Family format code plan)

      Exactly rounded base-ten exponential. NaR propagates.

      Instances For
        source
        @[inline]
        def FloatLib.Floats.ExecFloat.Posit.exp2Minus1 {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) :
        ExecFloat (Formats.Posit.Configured.Family format code plan)

        Base-two exponential minus one, rounded once after the subtraction. NaR propagates.

        Instances For
          source
          @[inline]
          def FloatLib.Floats.ExecFloat.Posit.exp10Minus1 {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) :
          ExecFloat (Formats.Posit.Configured.Family format code plan)

          Base-ten exponential minus one, rounded once after the subtraction. NaR propagates.

          Instances For