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