Documentation

Std.Data.Ord

Swaps less and greater ordering results

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.)

    Instances For

      Check whether the ordering is 'equal'.

      Instances For

        Check whether the ordering is 'not equal'.

        Instances For

          Check whether the ordering is 'less than'.

          Instances For

            Check whether the ordering is 'greater than'.

            Instances For

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

              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.

                Instances For
                  @[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.

                  Instances For
                    def Ord.toBEq {α : Type u_1} (ord : Ord α) :
                    BEq α

                    Derive a BEq instance from an Ord instance.

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

                      Derive an LT instance from an Ord instance.

                      Instances For
                        def Ord.toLE {α : Type u_1} :
                        Ord αLE α

                        Derive an LE instance from an Ord instance.

                        Instances For
                          def Ord.opposite {α : Type u_1} (ord : Ord α) :
                          Ord α

                          Invert the order of an Ord instance.

                          Instances For
                            def Ord.on {β : Type u_1} {α : Type u_2} (ord : Ord β) (f : αβ) :
                            Ord α

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

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

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

                              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₂.

                                Instances For