mathlib documentation

core / init.data.ordering.basic

source
inductive ordering  :
Type
source
@[protected, instance]
def ordering.has_repr  :
has_repr ordering
Equations
source
def ordering.swap  :
ordering → ordering
Equations
source
def ordering.or_else  :
ordering → 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
@[protected, instance]
def ordering.decidable_eq  :
decidable_eq ordering
Equations