Helper definitions and instances for Ordering

instance instReprOrdering_mathlib : Repr Ordering

Equations

• instReprOrdering_mathlib = { reprPrec := reprOrdering✝ }

@[inline]

def Ordering.orElse : Ordering → Ordering → Ordering

Combine two Orderings lexicographically.

Equations

• Ordering.lt.orElse x = Ordering.lt
• Ordering.eq.orElse x = x
• Ordering.gt.orElse x = Ordering.gt

def Ordering.toRel {α : Type u} [LT α] : Ordering → α → α → Prop

The relation corresponding to each Ordering constructor (e.g. .lt.toProp a b is a < b).

Equations

• Ordering.lt.toRel = fun (x1 x2 : α) => x1 < x2
• Ordering.eq.toRel = Eq
• Ordering.gt.toRel = fun (x1 x2 : α) => x1 > x2

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 α] [DecidableRel fun (x1 x2 : α) => x1 < x2] (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