mathlib documentation

core.init.data.ordering.basic

inductive ordering  :
Type

@[instance]

Equations
theorem ordering.swap_swap (o : ordering) :
o.swap.swap = o

def cmp_using {α : Type u} (lt : α → α → Prop) [decidable_rel lt] :
α → α → ordering

Equations
def cmp {α : Type u} [has_lt α] [decidable_rel has_lt.lt] :
α → α → ordering

Equations
@[instance]

Equations