TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Numerics.IEEEComparison

IEEE comparison predicates #

The truth tables in IEEE 754-2019 Tables 5.1–5.2 depend only on four possible relations: less, equal, greater, and unordered. This module shares those tables between numerical formats. Operand decoding and the invalid-operation flag belong to each format's API.

source
structure FloatLib.Numerics.IEEEComparison.Result :
Type

A predicate's truth value and the exceptions raised while evaluating it.

  • value : Bool

    The Boolean answer, including the predicate's unordered case.

  • status : IEEEStatus

    Exceptions raised by this comparison.

Instances For
    source
    def FloatLib.Numerics.IEEEComparison.instDecidableEqResult.decEq (x✝ x✝¹ : Result) :
    Decidable (x✝ = x✝¹)
    Instances For
      source
      @[instance_reducible]
      instance FloatLib.Numerics.IEEEComparison.instDecidableEqResult :
      DecidableEq Result
      source
      def FloatLib.Numerics.IEEEComparison.instReprResult.repr :
      Result → Nat → Std.Format
      Instances For
        source
        @[instance_reducible]
        instance FloatLib.Numerics.IEEEComparison.instReprResult :
        Repr Result
        source
        inductive FloatLib.Numerics.IEEEComparison.Predicate :
        Type

        Truth sets named by the IEEE quiet and signaling comparison operations.

        Instances For
          source
          @[instance_reducible]
          instance FloatLib.Numerics.IEEEComparison.instDecidableEqPredicate :
          DecidableEq Predicate
          source
          def FloatLib.Numerics.IEEEComparison.instReprPredicate.repr :
          Predicate → Nat → Std.Format
          Instances For
            source
            @[instance_reducible]
            instance FloatLib.Numerics.IEEEComparison.instReprPredicate :
            Repr Predicate
            source
            def FloatLib.Numerics.IEEEComparison.Predicate.accepts :
            Predicate → Option Ordering → Bool

            Whether a predicate accepts a relation; none denotes unordered operands.

            Instances For
              source
              theorem FloatLib.Numerics.IEEEComparison.accepts_notEqual (relation : Option Ordering) :
              Predicate.notEqual.accepts relation = !Predicate.equal.accepts relation

              Inequality is the complement of equality, including unordered inputs.

              source
              theorem FloatLib.Numerics.IEEEComparison.accepts_ordered (relation : Option Ordering) :
              Predicate.ordered.accepts relation = !Predicate.unordered.accepts relation

              Ordered and unordered are complementary predicates.

              source
              theorem FloatLib.Numerics.IEEEComparison.accepts_notGreater (relation : Option Ordering) :
              Predicate.notGreater.accepts relation = !Predicate.greater.accepts relation

              Not-greater includes unordered inputs and is the complement of greater-than.

              source
              theorem FloatLib.Numerics.IEEEComparison.accepts_notLess (relation : Option Ordering) :
              Predicate.notLess.accepts relation = !Predicate.less.accepts relation

              Not-less includes unordered inputs and is the complement of less-than.

              source
              theorem FloatLib.Numerics.IEEEComparison.accepts_lessUnordered (relation : Option Ordering) :
              Predicate.lessUnordered.accepts relation = !Predicate.greaterEqual.accepts relation

              Less-or-unordered complements greater-or-equal across all four relations.

              source
              theorem FloatLib.Numerics.IEEEComparison.accepts_greaterUnordered (relation : Option Ordering) :
              Predicate.greaterUnordered.accepts relation = !Predicate.lessEqual.accepts relation

              Greater-or-unordered complements less-or-equal across all four relations.