Helper definitions and instances for Ordering

ink

instance instReprOrdering : Repr Ordering

Equations

• instReprOrdering = { reprPrec := reprOrdering✝ }

ink

@[inline]

def Ordering.orElse : Ordering → Ordering → Ordering

Combine two Orderings lexicographically.

Equations

• Ordering.orElse x x = match x, x with | Ordering.lt, x => Ordering.lt | Ordering.eq, o => o | Ordering.gt, x => Ordering.gt

ink

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

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

Equations

• Ordering.toRel x = match (motive := Ordering → α → α → Prop) x with | Ordering.lt => fun x x_1 => x < x_1 | Ordering.eq => Eq | Ordering.gt => fun x x_1 => x > x_1

ink

def cmpUsing {α : Type u} (lt : α → α → Prop) [inst : 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

ink

def cmp {α : Type u} [inst : LT α] [inst : DecidableRel fun x x_1 => x < x_1] (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 x x_1 => x < x_1) a b