TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.Posit.Configured.Functions.Basic

Basic posit functions on the public configured carrier #

Every function uses the universal carrier/model codec. Static storage selection therefore does not alter numerical behavior, while users retain one ExecFloat.Posit (bits := n) type.

The public functions lift the corresponding model operations. The codec inverse laws ensure that decoding a result recovers the model result.

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

Lexicographic successor of the posit representation, with wrapping.

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

    Lexicographic predecessor of the posit representation, with wrapping.

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

      Standard posit absolute value.

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

        Standard posit sign function, returning NaR when the input is NaR.

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

          Standard nearest integer-valued posit, with ties to an even integer.

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

            Standard ceiling to an integer-valued posit.

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

              Standard floor to an integer-valued posit.

              Instances For
                source
                @[simp]
                theorem FloatLib.Floats.ExecFloat.Posit.prior_next {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)) :
                prior (next value) = value

                Taking the predecessor after the representation successor restores the original posit.

                source
                @[simp]
                theorem FloatLib.Floats.ExecFloat.Posit.next_prior {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)) :
                next (prior value) = value

                Taking the successor after the representation predecessor restores the original posit.

                source
                @[simp]
                theorem FloatLib.Floats.ExecFloat.Posit.abs_zero {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] :
                abs zero = zero

                Posit absolute value fixes the unique zero encoding.

                source
                @[simp]
                theorem FloatLib.Floats.ExecFloat.Posit.abs_nar {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] :
                abs nar = nar

                Posit absolute value propagates Not-a-Real.

                source
                @[simp]
                theorem FloatLib.Floats.ExecFloat.Posit.sign_zero {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] :
                sign zero = zero

                The posit sign function fixes the unique zero encoding.

                source
                @[simp]
                theorem FloatLib.Floats.ExecFloat.Posit.sign_nar {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] :
                sign nar = nar

                The posit sign function propagates Not-a-Real.

                source
                @[simp]
                theorem FloatLib.Floats.ExecFloat.Posit.nearestInt_zero {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] :
                nearestInt zero = zero

                Nearest-integer rounding fixes the unique posit zero.

                source
                @[simp]
                theorem FloatLib.Floats.ExecFloat.Posit.nearestInt_nar {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] :
                nearestInt nar = nar

                Nearest-integer rounding propagates posit Not-a-Real.

                source
                @[simp]
                theorem FloatLib.Floats.ExecFloat.Posit.ceil_zero {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] :
                ceil zero = zero

                Posit ceiling fixes the unique zero encoding.

                source
                @[simp]
                theorem FloatLib.Floats.ExecFloat.Posit.ceil_nar {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] :
                ceil nar = nar

                Posit ceiling propagates Not-a-Real.

                source
                @[simp]
                theorem FloatLib.Floats.ExecFloat.Posit.floor_zero {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] :
                floor zero = zero

                Posit floor fixes the unique zero encoding.

                source
                @[simp]
                theorem FloatLib.Floats.ExecFloat.Posit.floor_nar {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] :
                floor nar = nar

                Posit floor propagates Not-a-Real.