## Equations

- instReprOrdering_mathlib = { reprPrec := reprOrdering✝ }

**Alias** of `Ordering.then`

.

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

`Compares o a b`

means that `a`

and `b`

have the ordering relation `o`

between them, assuming
that the relation `a < b`

is defined.

## Equations

- Ordering.lt.Compares x✝ x = (x✝ < x)
- Ordering.eq.Compares x✝ x = (x✝ = x)
- Ordering.gt.Compares x✝ x = (x✝ > x)

## Instances For

**Alias** of `Ordering.Compares`

.

`Compares o a b`

means that `a`

and `b`

have the ordering relation `o`

between them, assuming
that the relation `a < b`

is defined.

## Equations

## Instances For

Lift a decidable relation to an `Ordering`

,
assuming that incomparable terms are `Ordering.eq`

.

## Equations

- cmpUsing lt a b = if lt a b then Ordering.lt else if lt b a then Ordering.gt else Ordering.eq