mathlib documentation

core / init.data.rbtree.basic

inductive rbnode (α : Type u) :
Type u
inductive rbnode.color  :
Type
@[instance]
Equations
def rbnode.depth {α : Type u} (f : ) :
rbnode α
Equations
def rbnode.min {α : Type u} :
rbnode αoption α
Equations
def rbnode.max {α : Type u} :
rbnode αoption α
Equations
def rbnode.fold {α : Type u} {β : Type v} (f : α → β → β) :
rbnode αβ → β
Equations
def rbnode.rev_fold {α : Type u} {β : Type v} (f : α → β → β) :
rbnode αβ → β
Equations
def rbnode.balance1 {α : Type u} :
rbnode αα → rbnode αα → rbnode αrbnode α
Equations
def rbnode.balance1_node {α : Type u} :
rbnode αα → rbnode αrbnode α
Equations
def rbnode.balance2 {α : Type u} :
rbnode αα → rbnode αα → rbnode αrbnode α
Equations
def rbnode.balance2_node {α : Type u} :
rbnode αα → rbnode αrbnode α
Equations
def rbnode.ins {α : Type u} (lt : α → α → Prop) [decidable_rel lt] :
rbnode αα → rbnode α
Equations
def rbnode.insert {α : Type u} (lt : α → α → Prop) [decidable_rel lt] (t : rbnode α) (x : α) :
Equations
def rbnode.mem {α : Type u} (lt : α → α → Prop) :
α → rbnode α → Prop
Equations
def rbnode.find {α : Type u} (lt : α → α → Prop) [decidable_rel lt] :
rbnode αα → option α
Equations
inductive rbnode.well_formed {α : Type u} (lt : α → α → Prop) :
rbnode α → Prop
def rbtree (α : Type u) (lt : α → α → Prop . "default_lt") :
Type u
Equations
def mk_rbtree (α : Type u) (lt : α → α → Prop . "default_lt") :
rbtree α lt
Equations
def rbtree.mem {α : Type u} {lt : α → α → Prop} (a : α) (t : rbtree α lt) :
Prop
Equations
@[instance]
def rbtree.has_mem {α : Type u} {lt : α → α → Prop} :
has_mem α (rbtree α lt)
Equations
def rbtree.mem_exact {α : Type u} {lt : α → α → Prop} (a : α) (t : rbtree α lt) :
Prop
Equations
def rbtree.depth {α : Type u} {lt : α → α → Prop} (f : ) (t : rbtree α lt) :
Equations
def rbtree.fold {α : Type u} {β : Type v} {lt : α → α → Prop} (f : α → β → β) :
rbtree α ltβ → β
Equations
def rbtree.rev_fold {α : Type u} {β : Type v} {lt : α → α → Prop} (f : α → β → β) :
rbtree α ltβ → β
Equations
def rbtree.empty {α : Type u} {lt : α → α → Prop} :
rbtree α ltbool
Equations
def rbtree.to_list {α : Type u} {lt : α → α → Prop} :
rbtree α ltlist α
Equations
def rbtree.min {α : Type u} {lt : α → α → Prop} :
rbtree α ltoption α
Equations
def rbtree.max {α : Type u} {lt : α → α → Prop} :
rbtree α ltoption α
Equations
@[instance]
def rbtree.has_repr {α : Type u} {lt : α → α → Prop} [has_repr α] :
Equations
def rbtree.insert {α : Type u} {lt : α → α → Prop} [decidable_rel lt] :
rbtree α ltα → rbtree α lt
Equations
def rbtree.find {α : Type u} {lt : α → α → Prop} [decidable_rel lt] :
rbtree α ltα → option α
Equations
def rbtree.contains {α : Type u} {lt : α → α → Prop} [decidable_rel lt] (t : rbtree α lt) (a : α) :
Equations
def rbtree.from_list {α : Type u} (l : list α) (lt : α → α → Prop . "default_lt") [decidable_rel lt] :
rbtree α lt
Equations
def rbtree_of {α : Type u} (l : list α) (lt : α → α → Prop . "default_lt") [decidable_rel lt] :
rbtree α lt
Equations