mathlib documentation

data.rbtree.init

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