mathlib documentation

core.init.data.rbtree.basic

inductive rbnode  :
Type uType u

inductive rbnode.color  :
Type

@[instance]

Equations
def rbnode.depth {α : Type u} :
()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} :
(α → β → β)rbnode αβ → β

Equations
def rbnode.rev_fold {α : Type u} {β : Type v} :
(α → β → β)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] :
rbnode αα → rbnode α

Equations
def rbnode.mem {α : Type u} :
(α → α → Prop)α → rbnode α → Prop

Equations
def rbnode.find {α : Type u} (lt : α → α → Prop) [decidable_rel lt] :
rbnode αα → option α

Equations
inductive rbnode.well_formed {α : Type u} :
(α → α → Prop)rbnode α → Prop

def rbtree (α : Type u) :
(α → α → 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} :
α → 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} :
α → rbtree α lt → Prop

Equations
def rbtree.depth {α : Type u} {lt : α → α → Prop} :
()rbtree α lt

Equations
def rbtree.fold {α : Type u} {β : Type v} {lt : α → α → Prop} :
(α → β → β)rbtree α ltβ → β

Equations
def rbtree.rev_fold {α : Type u} {β : Type v} {lt : α → α → Prop} :
(α → β → β)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] :
rbtree α ltα → bool

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