Documentation

Std.Data.RBTree

noncomputable def Std.RBTree (α : Type u) (cmp : ααOrdering) :
Type u
Equations
instance Std.instInhabitedRBTree {α : Type u_1} {p : ααOrdering} :
Equations
  • Std.instInhabitedRBTree = { default := Std.RBMap.empty }
@[inline]
def Std.mkRBTree (α : Type u) (cmp : ααOrdering) :
Std.RBTree α cmp
Equations
instance Std.instEmptyCollectionRBTree (α : Type u) (cmp : ααOrdering) :
Equations
@[inline]
def Std.RBTree.empty {α : Type u} {cmp : ααOrdering} :
Std.RBTree α cmp
Equations
  • Std.RBTree.empty = Std.RBMap.empty
@[inline]
def Std.RBTree.depth {α : Type u} {cmp : ααOrdering} (f : NatNatNat) (t : Std.RBTree α cmp) :
Equations
@[inline]
def Std.RBTree.fold {α : Type u} {β : Type v} {cmp : ααOrdering} (f : βαβ) (init : β) (t : Std.RBTree α cmp) :
β
Equations
@[inline]
def Std.RBTree.revFold {α : Type u} {β : Type v} {cmp : ααOrdering} (f : βαβ) (init : β) (t : Std.RBTree α cmp) :
β
Equations
@[inline]
def Std.RBTree.foldM {α : Type u} {β : Type v} {cmp : ααOrdering} {m : Type vType w} [inst : Monad m] (f : βαm β) (init : β) (t : Std.RBTree α cmp) :
m β
Equations
@[inline]
def Std.RBTree.forM {α : Type u} {cmp : ααOrdering} {m : Type vType w} [inst : Monad m] (f : αm PUnit) (t : Std.RBTree α cmp) :
Equations
@[inline]
def Std.RBTree.forIn {α : Type u} {cmp : ααOrdering} {m : Type u_1Type u_2} {σ : Type u_1} [inst : Monad m] (t : Std.RBTree α cmp) (init : σ) (f : ασm (ForInStep σ)) :
m σ
Equations
instance Std.RBTree.instForInRBTree {α : Type u} {cmp : ααOrdering} {m : Type u_1Type u_2} :
ForIn m (Std.RBTree α cmp) α
Equations
  • Std.RBTree.instForInRBTree = { forIn := fun {β} [Monad m] => Std.RBTree.forIn }
@[inline]
def Std.RBTree.isEmpty {α : Type u} {cmp : ααOrdering} (t : Std.RBTree α cmp) :
Equations
@[specialize]
def Std.RBTree.toList {α : Type u} {cmp : ααOrdering} (t : Std.RBTree α cmp) :
List α
Equations
@[specialize]
def Std.RBTree.toArray {α : Type u} {cmp : ααOrdering} (t : Std.RBTree α cmp) :
Equations
@[inline]
def Std.RBTree.min {α : Type u} {cmp : ααOrdering} (t : Std.RBTree α cmp) :
Equations
@[inline]
def Std.RBTree.max {α : Type u} {cmp : ααOrdering} (t : Std.RBTree α cmp) :
Equations
instance Std.RBTree.instReprRBTree {α : Type u} {cmp : ααOrdering} [inst : Repr α] :
Repr (Std.RBTree α cmp)
Equations
@[inline]
def Std.RBTree.insert {α : Type u} {cmp : ααOrdering} (t : Std.RBTree α cmp) (a : α) :
Std.RBTree α cmp
Equations
@[inline]
def Std.RBTree.erase {α : Type u} {cmp : ααOrdering} (t : Std.RBTree α cmp) (a : α) :
Std.RBTree α cmp
Equations
@[specialize]
def Std.RBTree.ofList {α : Type u} {cmp : ααOrdering} :
List αStd.RBTree α cmp
Equations
@[inline]
def Std.RBTree.find? {α : Type u} {cmp : ααOrdering} (t : Std.RBTree α cmp) (a : α) :
Equations
@[inline]
def Std.RBTree.contains {α : Type u} {cmp : ααOrdering} (t : Std.RBTree α cmp) (a : α) :
Equations
def Std.RBTree.fromList {α : Type u} (l : List α) (cmp : ααOrdering) :
Std.RBTree α cmp
Equations
@[inline]
def Std.RBTree.all {α : Type u} {cmp : ααOrdering} (t : Std.RBTree α cmp) (p : αBool) :
Equations
@[inline]
def Std.RBTree.any {α : Type u} {cmp : ααOrdering} (t : Std.RBTree α cmp) (p : αBool) :
Equations
def Std.RBTree.subset {α : Type u} {cmp : ααOrdering} (t₁ : Std.RBTree α cmp) (t₂ : Std.RBTree α cmp) :
Equations
def Std.RBTree.seteq {α : Type u} {cmp : ααOrdering} (t₁ : Std.RBTree α cmp) (t₂ : Std.RBTree α cmp) :
Equations
def Std.rbtreeOf {α : Type u} (l : List α) (cmp : ααOrdering) :
Std.RBTree α cmp
Equations