Documentation

Init.Data.Ord

inductive Ordering :
Instances For
    class Ord (α : Type u) :
    Instances
      @[inline]
      def compareOfLessAndEq {α : Type u_1} (x : α) (y : α) [LT α] [Decidable (x < y)] [DecidableEq α] :
      Equations
      Instances For
        instance instOrdNat :
        Equations
        instance instOrdInt :
        Equations
        instance instOrdBool :
        Equations
        Equations
        instance instOrdFin (n : Nat) :
        Ord (Fin n)
        Equations
        Equations
        Equations
        Equations
        Equations
        Equations
        instance instOrdChar :
        Equations
        def lexOrd {α : Type u_1} {β : Type u_2} [Ord α] [Ord β] :
        Ord (α × β)

        The lexicographic order on pairs.

        Equations
        • lexOrd = { compare := fun (p1 p2 : α × β) => match compare p1.fst p2.fst with | Ordering.eq => compare p1.snd p2.snd | o => o }
        Instances For
          def ltOfOrd {α : Type u_1} [Ord α] :
          LT α
          Equations
          Instances For
            instance instDecidableRelLtLtOfOrd {α : Type u_1} [Ord α] :
            Equations
            Equations
            Instances For
              def leOfOrd {α : Type u_1} [Ord α] :
              LE α
              Equations
              Instances For
                instance instDecidableRelLeLeOfOrd {α : Type u_1} [Ord α] :
                Equations