Documentation

Init.Data.Ord

source
inductive Ordering :
Type
Instances For
    source
    instance instInhabitedOrdering :
    Inhabited Ordering
    source
    instance instBEqOrdering :
    BEq Ordering
    source
    class Ord (α : Type u) :
    Type u
    Instances
      source
      @[inline]
      def compareOfLessAndEq {α : Type u_1} (x : α) (y : α) [LT α] [Decidable (x < y)] [DecidableEq α] :
      Ordering
      Instances For
        source
        instance instOrdNat :
        Ord Nat
        source
        instance instOrdInt :
        Ord Int
        source
        instance instOrdBool :
        Ord Bool
        source
        instance instOrdString :
        Ord String
        source
        instance instOrdFin (n : Nat) :
        Ord (Fin n)
        source
        instance instOrdUInt8 :
        Ord UInt8
        source
        instance instOrdUInt16 :
        Ord UInt16
        source
        instance instOrdUInt32 :
        Ord UInt32
        source
        instance instOrdUInt64 :
        Ord UInt64
        source
        instance instOrdUSize :
        Ord USize
        source
        instance instOrdChar :
        Ord Char
        source
        def lexOrd {α : Type u_1} {β : Type u_2} [Ord α] [Ord β] :
        Ord (α × β)

        The lexicographic order on pairs.

        Instances For
          source
          def ltOfOrd {α : Type u_1} [Ord α] :
          LT α
          Instances For
            source
            instance instDecidableRelLtLtOfOrd {α : Type u_1} [Ord α] :
            DecidableRel LT.lt
            source
            def Ordering.isLE :
            Ordering → Bool
            Instances For
              source
              def leOfOrd {α : Type u_1} [Ord α] :
              LE α
              Instances For
                source
                instance instDecidableRelLeLeOfOrd {α : Type u_1} [Ord α] :
                DecidableRel LE.le