mathlib3 documentation

data.rbtree.init

inductive rbnode (α : Type u) :
Instances for rbnode
inductive rbnode.color  :
Instances for rbnode.color
@[protected, instance]
Equations
def rbnode.depth {α : Type u} (f : ) :
Equations
@[protected]
def rbnode.min {α : Type u} :
Equations
@[protected]
def rbnode.max {α : Type u} :
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} :
Equations
def rbnode.balance2 {α : Type u} :
rbnode α α rbnode α α rbnode α rbnode α
Equations
def rbnode.balance2_node {α : Type u} :
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") :
Equations
Instances for rbtree
def mk_rbtree (α : Type u) (lt : α α Prop . "default_lt") :
rbtree α lt
Equations
@[protected]
def rbtree.mem {α : Type u} {lt : α α Prop} (a : α) (t : rbtree α lt) :
Prop
Equations
@[protected, 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} :
Equations
def rbtree.to_list {α : Type u} {lt : α α Prop} :
rbtree α lt list α
Equations
@[protected]
def rbtree.min {α : Type u} {lt : α α Prop} :
rbtree α lt option α
Equations
@[protected]
def rbtree.max {α : Type u} {lt : α α Prop} :
rbtree α lt option α
Equations
@[protected, 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