TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.DecimalInterchange.Comparison.Runtime

Exact decimal comparisons #

IEEE 754-2019 §5.6.1 requires the 22 predicates of Tables 5.1–5.2. Comparison uses exact rational values extended by two infinities; it ignores finite cohorts and equates signed zeros. NaNs are unordered. Quiet comparisons raise invalid only for signaling NaNs; signaling comparisons raise invalid for either kind of NaN. No other exception is raised.

source
@[reducible, inline]
abbrev FloatLib.Floats.Formats.DecimalInterchange.NumericValue :
Type

Exact ordered values, with negative and positive infinity at the endpoints.

Instances For
    source
    def FloatLib.Floats.Formats.DecimalInterchange.Datum.numericValue? :
    Datum → Option NumericValue

    Ordered numerical meaning. NaN is absent, rather than assigned an ordered value.

    Instances For
      source
      def FloatLib.Floats.Formats.DecimalInterchange.Comparison.relation (x y : Datum) :
      Option Ordering

      Four comparison relations: none is unordered, and some is less, equal or greater.

      Instances For
        source
        @[reducible, inline]
        abbrev FloatLib.Floats.Formats.DecimalInterchange.Comparison.Predicate :
        Type

        Truth sets named in the IEEE comparison tables.

        Instances For
          source
          @[reducible, inline]
          abbrev FloatLib.Floats.Formats.DecimalInterchange.Comparison.Result :
          Type

          A predicate result and its default IEEE exception flags.

          Instances For
            source
            def FloatLib.Floats.Formats.DecimalInterchange.Comparison.quiet (predicate : Predicate) (x y : Datum) :
            Result

            Evaluate a quiet predicate, signaling invalid only for an sNaN operand.

            Instances For
              source
              def FloatLib.Floats.Formats.DecimalInterchange.Comparison.signaling (predicate : Predicate) (x y : Datum) :
              Result

              Evaluate a signaling predicate, signaling invalid for any NaN operand.

              Instances For
                source
                def FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.compareQuietEqual (x y : Datum) :
                Comparison.Result

                Quiet equality; signed zeros and equal-valued cohorts compare equal.

                Instances For
                  source
                  def FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.compareQuietNotEqual (x y : Datum) :
                  Comparison.Result

                  Quiet inequality, true on unordered operands.

                  Instances For
                    source
                    def FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.compareQuietGreater (x y : Datum) :
                    Comparison.Result

                    Quiet greater-than comparison.

                    Instances For
                      source
                      def FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.compareQuietGreaterEqual (x y : Datum) :
                      Comparison.Result

                      Quiet greater-than-or-equal comparison.

                      Instances For
                        source
                        def FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.compareQuietLess (x y : Datum) :
                        Comparison.Result

                        Quiet less-than comparison.

                        Instances For
                          source
                          def FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.compareQuietLessEqual (x y : Datum) :
                          Comparison.Result

                          Quiet less-than-or-equal comparison.

                          Instances For
                            source
                            def FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.compareQuietUnordered (x y : Datum) :
                            Comparison.Result

                            Quiet test for an unordered pair.

                            Instances For
                              source
                              def FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.compareQuietOrdered (x y : Datum) :
                              Comparison.Result

                              Quiet test for an ordered pair.

                              Instances For
                                source
                                def FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.compareQuietLessUnordered (x y : Datum) :
                                Comparison.Result

                                Quiet less-than-or-unordered comparison, the complement of greater-than-or-equal.

                                Instances For
                                  source
                                  def FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.compareQuietNotGreater (x y : Datum) :
                                  Comparison.Result

                                  Quiet complement of greater-than, including unordered pairs.

                                  Instances For
                                    source
                                    def FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.compareQuietNotLess (x y : Datum) :
                                    Comparison.Result

                                    Quiet complement of less-than, including unordered pairs.

                                    Instances For
                                      source
                                      def FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.compareQuietGreaterUnordered (x y : Datum) :
                                      Comparison.Result

                                      Quiet greater-than-or-unordered comparison, the complement of less-than-or-equal.

                                      Instances For
                                        source
                                        def FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.compareSignalingEqual (x y : Datum) :
                                        Comparison.Result

                                        Signaling equality.

                                        Instances For
                                          source
                                          def FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.compareSignalingNotEqual (x y : Datum) :
                                          Comparison.Result

                                          Signaling inequality, true on unordered operands.

                                          Instances For
                                            source
                                            def FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.compareSignalingGreater (x y : Datum) :
                                            Comparison.Result

                                            Signaling greater-than comparison.

                                            Instances For
                                              source
                                              def FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.compareSignalingGreaterEqual (x y : Datum) :
                                              Comparison.Result

                                              Signaling greater-than-or-equal comparison.

                                              Instances For
                                                source
                                                def FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.compareSignalingLess (x y : Datum) :
                                                Comparison.Result

                                                Signaling less-than comparison.

                                                Instances For
                                                  source
                                                  def FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.compareSignalingLessEqual (x y : Datum) :
                                                  Comparison.Result

                                                  Signaling less-than-or-equal comparison.

                                                  Instances For
                                                    source
                                                    def FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.compareSignalingNotGreater (x y : Datum) :
                                                    Comparison.Result

                                                    Signaling complement of greater-than.

                                                    Instances For
                                                      source
                                                      def FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.compareSignalingNotLess (x y : Datum) :
                                                      Comparison.Result

                                                      Signaling complement of less-than.

                                                      Instances For
                                                        source
                                                        def FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.compareSignalingLessUnordered (x y : Datum) :
                                                        Comparison.Result

                                                        Signaling less-than-or-unordered comparison.

                                                        Instances For
                                                          source
                                                          def FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.compareSignalingGreaterUnordered (x y : Datum) :
                                                          Comparison.Result

                                                          Signaling greater-than-or-unordered comparison.

                                                          Instances For