TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

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

Configured posit algebraic functions #

These functions use the exact rational algebraic kernels through the selected carrier's model codec. Storage selection does not introduce additional rounding. NaR and invalid real domains have the same behavior as the model operations.

source
@[inline]
def FloatLib.Floats.ExecFloat.Posit.rSqrt {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)

Reciprocal square root, rounded once; nonpositive inputs and NaR produce NaR.

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

    Euclidean hypotenuse, rounded once after an exact sum of squares; NaR propagates.

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

      Fused triple multiplication, with one final rounding and NaR propagation.

      Instances For
        source
        @[inline]
        def FloatLib.Floats.ExecFloat.Posit.rootN {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)) (degree : ℤ) :
        ExecFloat (Formats.Posit.Configured.Family format code plan)

        Integer root, rounded once, taking the signed real root for odd degrees. Degree zero, even roots of negative inputs, negative-degree roots of zero, and NaR inputs produce NaR.

        Instances For
          source
          @[inline]
          def FloatLib.Floats.ExecFloat.Posit.powInt {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)) (exponent : ℤ) :
          ExecFloat (Formats.Posit.Configured.Family format code plan)

          Fixed integer power, rounded once; NaR and zero to negative powers produce NaR.

          Instances For
            source
            @[inline]
            def FloatLib.Floats.ExecFloat.Posit.compound {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)) (exponent : ℤ) :
            ExecFloat (Formats.Posit.Configured.Family format code plan)

            Compound (1 + x) ^ n, rounding only the final result. NaR propagates, and x = -1 with negative exponent produces NaR. Exponent zero gives one on every finite input.

            Instances For