TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.ExecFloat.Comparison

Optional comparison capability for ExecFloat #

Comparison is format-defined rather than imposed by the universal carrier. IEEE binary formats use an unordered result for NaN, while standard posits use their total signed-word order, including NaR. Formats for which no comparison has been specified simply do not install this capability.

The public functions in this module give clients one spelling independently of the numerical family:

ExecFloat.compare left right
ExecFloat.compareEqual left right
ExecFloat.compareLess left right

Option Ordering retains the distinction between an ordered result and an unordered comparison. The Boolean predicates then follow each format's installed comparison without assuming IEEE, posit, real-number, or bitwise semantics.

source
class FloatLib.Floats.ExecFloat.Comparison (F : Type u) [Numerics.EncodedFormat F] :
Type u_1

Format-defined comparison for executable values.

none means unordered. A format with a total order returns some for every pair.

Instances
    source
    @[inline]
    def FloatLib.Floats.ExecFloat.compare {F : Type u} [Numerics.EncodedFormat F] [self : Comparison F] (left right : ExecFloat F) :
    Option Ordering

    Compare two executable values according to their format's comparison semantics.

    Instances For
      source
      @[inline]
      def FloatLib.Floats.ExecFloat.compareEqual {F : Type u} [Numerics.EncodedFormat F] [Comparison F] (left right : ExecFloat F) :
      Bool

      Format-defined numerical equality.

      For an unordered comparison this is false; consequently IEEE NaNs compare unequal. A format whose comparison is total may choose to include exceptional stored values in its equality.

      Instances For
        source
        @[inline]
        def FloatLib.Floats.ExecFloat.compareNotEqual {F : Type u} [Numerics.EncodedFormat F] [Comparison F] (left right : ExecFloat F) :
        Bool

        Format-defined numerical inequality.

        This is the Boolean complement of compareEqual, so unordered pairs compare unequal.

        Instances For
          source
          @[inline]
          def FloatLib.Floats.ExecFloat.compareLess {F : Type u} [Numerics.EncodedFormat F] [Comparison F] (left right : ExecFloat F) :
          Bool

          Strict less-than; unordered comparisons return false.

          Instances For
            source
            @[inline]
            def FloatLib.Floats.ExecFloat.compareLessEqual {F : Type u} [Numerics.EncodedFormat F] [Comparison F] (left right : ExecFloat F) :
            Bool

            Less-than-or-equal; unordered comparisons return false.

            Instances For
              source
              @[inline]
              def FloatLib.Floats.ExecFloat.compareGreater {F : Type u} [Numerics.EncodedFormat F] [Comparison F] (left right : ExecFloat F) :
              Bool

              Strict greater-than; unordered comparisons return false.

              Instances For
                source
                @[inline]
                def FloatLib.Floats.ExecFloat.compareGreaterEqual {F : Type u} [Numerics.EncodedFormat F] [Comparison F] (left right : ExecFloat F) :
                Bool

                Greater-than-or-equal; unordered comparisons return false.

                Instances For