mathlib documentation

core.init.data.ordering.basic

source
inductive ordering  :
Type

source
@[instance]
def ordering.has_repr  :
has_repr ordering

Equations
source
def ordering.swap (a : ordering) :
ordering

Equations
source
def ordering.or_else (a a_1 : ordering) :
ordering

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

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

Equations
source
def cmp {α : Type u} [has_lt α] [decidable_rel has_lt.lt] (a b : α) :
ordering

Equations
source
@[instance]
def ordering.decidable_eq  :
decidable_eq ordering

Equations