# Helper definitions and instances for `Ordering` #

source
def Ordering.Compares {α : Type u_1} [LT α] :
Ordering → α → α → Prop

`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

source
@[simp]
theorem Ordering.compares_lt {α : Type u_1} [LT α] (a b : α) :
lt.Compares a b = (a < b)
source
@[simp]
theorem Ordering.compares_eq {α : Type u_1} [LT α] (a b : α) :
eq.Compares a b = (a = b)
source
@[simp]
theorem Ordering.compares_gt {α : Type u_1} [LT α] (a b : α) :
gt.Compares a b = (a > b)
source
@[macro_inline]
def Ordering.dthen (o : Ordering) :
(o = eq → Ordering) → Ordering

`o₁.dthen fun h => o₂(h)` is like `o₁.then o₂` but `o₂` is allowed to depend on `h : o₁ = .eq`.

Equations

- Ordering.eq.dthen f = f ⋯
- x✝¹.dthen x✝ = x✝¹

Instances For

source
def cmpUsing {α : Type u} (lt : α → α → Prop) [DecidableRel lt] (a b : α) :
Ordering

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

Instances For

source
def cmp {α : Type u} [LT α] [DecidableLT α] (a b : α) :
Ordering

Construct an `Ordering` from a type with a decidable `LT` instance, assuming that incomparable terms are `Ordering.eq`.

Equations

- cmp a b = cmpUsing (fun (x1 x2 : α) => x1 < x2) a b

Instances For