Documentation

Init.Data.Ord

inductive Ordering :
Instances For
    Equations
    • x.instDecidableEq y = if h : x.toCtorIdx = y.toCtorIdx then isTrue else isFalse

    Swaps less and greater ordering results

    Equations
    Instances For
      @[macro_inline]

      If o₁ and o₂ are Ordering, then o₁.then o₂ returns o₁ unless it is .eq, in which case it returns o₂. Additionally, it has "short-circuiting" semantics similar to boolean x && y: if o₁ is not .eq then the expression for o₂ is not evaluated. This is a useful primitive for constructing lexicographic comparator functions:

      structure Person where
        name : String
        age : Nat
      
      instance : Ord Person where
        compare a b := (compare a.name b.name).then (compare b.age a.age)
      

      This example will sort people first by name (in ascending order) and will sort people with the same name by age (in descending order). (If all fields are sorted ascending and in the same order as they are listed in the structure, you can also use deriving Ord on the structure definition for the same effect.)

      Equations
      Instances For

        Check whether the ordering is 'equal'.

        Equations
        Instances For

          Check whether the ordering is 'not equal'.

          Equations
          Instances For

            Check whether the ordering is 'less than or equal to'.

            Equations
            Instances For

              Check whether the ordering is 'less than'.

              Equations
              Instances For

                Check whether the ordering is 'greater than'.

                Equations
                Instances For

                  Check whether the ordering is 'greater than or equal'.

                  Equations
                  Instances For
                    @[inline]
                    def compareOfLessAndEq {α : Type u_1} (x : α) (y : α) [LT α] [Decidable (x < y)] [DecidableEq α] :

                    Yields an Ordering s.t. x < y corresponds to Ordering.lt / Ordering.gt and x = y corresponds to Ordering.eq.

                    Equations
                    Instances For
                      @[inline]
                      def compareOfLessAndBEq {α : Type u_1} (x : α) (y : α) [LT α] [Decidable (x < y)] [BEq α] :

                      Yields an Ordering s.t. x < y corresponds to Ordering.lt / Ordering.gt and x == y corresponds to Ordering.eq.

                      Equations
                      Instances For
                        @[inline]
                        def compareLex {α : Sort u_1} {β : Sort u_2} (cmp₁ : αβOrdering) (cmp₂ : αβOrdering) (a : α) (b : β) :

                        Compare a and b lexicographically by cmp₁ and cmp₂. a and b are first compared by cmp₁. If this returns 'equal', a and b are compared by cmp₂ to break the tie.

                        Equations
                        • compareLex cmp₁ cmp₂ a b = (cmp₁ a b).then (cmp₂ a b)
                        Instances For
                          class Ord (α : Type u) :

                          Ord α provides a computable total order on α, in terms of the compare : α → α → Ordering function.

                          Typically instances will be transitive, reflexive, and antisymmetric, but this is not enforced by the typeclass.

                          There is a derive handler, so appending deriving Ord to an inductive type or structure will attempt to create an Ord instance.

                          • compare : ααOrdering

                            Compare two elements in α using the comparator contained in an [Ord α] instance.

                          Instances
                            @[inline]
                            def compareOn {β : Type u_1} {α : Sort u_2} [ord : Ord β] (f : αβ) (x : α) (y : α) :

                            Compare x and y by comparing f x and f y.

                            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
                              instance instOrdOption {α : Type u_1} [Ord α] :
                              Ord (Option α)
                              Equations
                              • One or more equations did not get rendered due to their size.
                              def lexOrd {α : Type u_1} {β : Type u_2} [Ord α] [Ord β] :
                              Ord (α × β)

                              The lexicographic order on pairs.

                              Equations
                              Instances For
                                def ltOfOrd {α : Type u_1} [Ord α] :
                                LT α
                                Equations
                                Instances For
                                  instance instDecidableRelLt {α : Type u_1} [Ord α] :
                                  Equations
                                  def leOfOrd {α : Type u_1} [Ord α] :
                                  LE α
                                  Equations
                                  Instances For
                                    instance instDecidableRelLe {α : Type u_1} [Ord α] :
                                    Equations
                                    def Ord.toBEq {α : Type u_1} (ord : Ord α) :
                                    BEq α

                                    Derive a BEq instance from an Ord instance.

                                    Equations
                                    Instances For
                                      def Ord.toLT {α : Type u_1} :
                                      Ord αLT α

                                      Derive an LT instance from an Ord instance.

                                      Equations
                                      • x.toLT = ltOfOrd
                                      Instances For
                                        def Ord.toLE {α : Type u_1} :
                                        Ord αLE α

                                        Derive an LE instance from an Ord instance.

                                        Equations
                                        • x.toLE = leOfOrd
                                        Instances For
                                          def Ord.opposite {α : Type u_1} (ord : Ord α) :
                                          Ord α

                                          Invert the order of an Ord instance.

                                          Equations
                                          • ord.opposite = { compare := fun (x y : α) => compare y x }
                                          Instances For
                                            def Ord.on {β : Type u_1} {α : Type u_2} :
                                            Ord β(αβ)Ord α

                                            ord.on f compares x and y by comparing f x and f y according to ord.

                                            Equations
                                            Instances For
                                              def Ord.lex {α : Type u_1} {β : Type u_2} :
                                              Ord αOrd βOrd (α × β)

                                              Derive the lexicographic order on products α × β from orders for α and β.

                                              Equations
                                              • x✝.lex x = lexOrd
                                              Instances For
                                                def Ord.lex' {α : Type u_1} (ord₁ : Ord α) (ord₂ : Ord α) :
                                                Ord α

                                                Create an order which compares elements first by ord₁ and then, if this returns 'equal', by ord₂.

                                                Equations
                                                • ord₁.lex' ord₂ = { compare := compareLex compare compare }
                                                Instances For
                                                  def Ord.arrayOrd {α : Type u_1} [a : Ord α] :
                                                  Ord (Array α)

                                                  Creates an order which compares elements of an Array in lexicographic order.

                                                  Equations
                                                  • Ord.arrayOrd = { compare := fun (x y : Array α) => let x_1 := a.toLT; let x_2 := a.toBEq; compareOfLessAndBEq x.toList y.toList }
                                                  Instances For