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.

Certified logarithm enclosures decide boundary comparisons before exact algebraic fallback. Small integer exponents use direct exact rational arithmetic before the single final rounding. Fallback cost depends on the numerical numerator and denominator of the decoded exponent; there is no resource-bound completion guarantee.

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. Inconclusive enclosures use exact comparison fallback.

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. Hard fallback cases can be expensive.

    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. Hard fallback cases can be expensive.

      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, with a single rounding after 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, with a single rounding after subtraction; NaR propagates.

          Instances For