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] (a b : α) :
Equations
def cmp {α : Type u} [has_lt α] [decidable_rel has_lt.lt] (a b : α) :
Equations
@[instance]
Equations