Helper definitions and instances for Ordering

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

@[simp]

theorem Ordering.compares_lt {α : Type u_1} [LT α] (a b : α) : lt.Compares a b = (a < b)

@[simp]

theorem Ordering.compares_eq {α : Type u_1} [LT α] (a b : α) : eq.Compares a b = (a = b)

@[simp]

theorem Ordering.compares_gt {α : Type u_1} [LT α] (a b : α) : gt.Compares a b = (a > b)

@[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✝¹

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

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