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