Documentation

Std.Data.RBMap

inductive Std.Rbcolor :
Type
inductive Std.RBNode (α : Type u) (β : αType v) :
Type (max u v)
def Std.RBNode.depth {α : Type u} {β : αType v} (f : NatNatNat) :
Std.RBNode α βNat
Equations
def Std.RBNode.min {α : Type u} {β : αType v} :
Std.RBNode α βOption ((k : α) × β k)
Equations
def Std.RBNode.max {α : Type u} {β : αType v} :
Std.RBNode α βOption ((k : α) × β k)
Equations
@[specialize]
def Std.RBNode.fold {α : Type u} {β : αType v} {σ : Type w} (f : σ(k : α) → β kσ) (init : σ) :
Std.RBNode α βσ
Equations
@[specialize]
def Std.RBNode.forM {α : Type u} {β : αType v} {m : TypeType u_1} [inst : Monad m] (f : (k : α) → β km Unit) :
Std.RBNode α βm Unit
Equations
@[specialize]
def Std.RBNode.foldM {α : Type u} {β : αType v} {σ : Type w} {m : Type wType u_1} [inst : Monad m] (f : σ(k : α) → β km σ) (init : σ) :
Std.RBNode α βm σ
Equations
@[inline]
def Std.RBNode.forIn {α : Type u} {β : αType v} {σ : Type w} {m : Type wType u_1} [inst : Monad m] (as : Std.RBNode α β) (init : σ) (f : (k : α) → β kσm (ForInStep σ)) :
m σ
Equations
@[specialize]
def Std.RBNode.forIn.visit {α : Type u} {β : αType v} {σ : Type w} {m : Type wType u_1} [inst : Monad m] (f : (k : α) → β kσm (ForInStep σ)) :
Std.RBNode α βσm (ForInStep σ)
Equations
@[specialize]
def Std.RBNode.revFold {α : Type u} {β : αType v} {σ : Type w} (f : σ(k : α) → β kσ) (init : σ) :
Std.RBNode α βσ
Equations
@[specialize]
def Std.RBNode.all {α : Type u} {β : αType v} (p : (k : α) → β kBool) :
Std.RBNode α βBool
Equations
@[specialize]
def Std.RBNode.any {α : Type u} {β : αType v} (p : (k : α) → β kBool) :
Std.RBNode α βBool
Equations
def Std.RBNode.singleton {α : Type u} {β : αType v} (k : α) (v : β k) :
Equations
@[inline]
def Std.RBNode.balance1 {α : Type u} {β : αType v} (a : α) :
β aStd.RBNode α βStd.RBNode α βStd.RBNode α β
Equations
@[inline]
def Std.RBNode.balance2 {α : Type u} {β : αType v} :
(a : Std.RBNode α β) → (a : α) → β aStd.RBNode α βStd.RBNode α β
Equations
def Std.RBNode.isRed {α : Type u} {β : αType v} :
Std.RBNode α βBool
Equations
def Std.RBNode.isBlack {α : Type u} {β : αType v} :
Std.RBNode α βBool
Equations
@[specialize]
def Std.RBNode.ins {α : Type u} {β : αType v} (cmp : ααOrdering) :
Std.RBNode α β(k : α) → β kStd.RBNode α β
Equations
def Std.RBNode.setBlack {α : Type u} {β : αType v} :
Std.RBNode α βStd.RBNode α β
Equations
@[specialize]
def Std.RBNode.insert {α : Type u} {β : αType v} (cmp : ααOrdering) (t : Std.RBNode α β) (k : α) (v : β k) :
Equations
def Std.RBNode.setRed {α : Type u} {β : αType v} :
Std.RBNode α βStd.RBNode α β
Equations
def Std.RBNode.balLeft {α : Type u} {β : αType v} :
Std.RBNode α β(k : α) → β kStd.RBNode α βStd.RBNode α β
Equations
def Std.RBNode.balRight {α : Type u} {β : αType v} (l : Std.RBNode α β) (k : α) (v : β k) (r : Std.RBNode α β) :
Equations
partial def Std.RBNode.appendTrees {α : Type u} {β : αType v} :
Std.RBNode α βStd.RBNode α βStd.RBNode α β
@[specialize]
def Std.RBNode.del {α : Type u} {β : αType v} (cmp : ααOrdering) (x : α) :
Std.RBNode α βStd.RBNode α β
Equations
@[specialize]
def Std.RBNode.erase {α : Type u} {β : αType v} (cmp : ααOrdering) (x : α) (t : Std.RBNode α β) :
Equations
@[specialize]
def Std.RBNode.findCore {α : Type u} {β : αType v} (cmp : ααOrdering) :
Std.RBNode α β(k : α) → Option ((k : α) × β k)
Equations
@[specialize]
def Std.RBNode.find {α : Type u} (cmp : ααOrdering) {β : Type v} :
(Std.RBNode α fun x => β) → αOption β
Equations
@[specialize]
def Std.RBNode.lowerBound {α : Type u} {β : αType v} (cmp : ααOrdering) :
Std.RBNode α βαOption (Sigma β)Option (Sigma β)
Equations
inductive Std.RBNode.WellFormed {α : Type u} {β : αType v} (cmp : ααOrdering) :
Std.RBNode α βProp
noncomputable def Std.RBMap (α : Type u) (β : Type v) (cmp : ααOrdering) :
Type (max u v)
Equations
@[inline]
def Std.mkRBMap (α : Type u) (β : Type v) (cmp : ααOrdering) :
Std.RBMap α β cmp
Equations
@[inline]
def Std.RBMap.empty {α : Type u} {β : Type v} {cmp : ααOrdering} :
Std.RBMap α β cmp
Equations
instance Std.instEmptyCollectionRBMap (α : Type u) (β : Type v) (cmp : ααOrdering) :
Equations
def Std.RBMap.depth {α : Type u} {β : Type v} {cmp : ααOrdering} (f : NatNatNat) (t : Std.RBMap α β cmp) :
Equations
@[inline]
def Std.RBMap.fold {α : Type u} {β : Type v} {σ : Type w} {cmp : ααOrdering} (f : σαβσ) (init : σ) :
Std.RBMap α β cmpσ
Equations
@[inline]
def Std.RBMap.revFold {α : Type u} {β : Type v} {σ : Type w} {cmp : ααOrdering} (f : σαβσ) (init : σ) :
Std.RBMap α β cmpσ
Equations
@[inline]
def Std.RBMap.foldM {α : Type u} {β : Type v} {σ : Type w} {cmp : ααOrdering} {m : Type wType u_1} [inst : Monad m] (f : σαβm σ) (init : σ) :
Std.RBMap α β cmpm σ
Equations
@[inline]
def Std.RBMap.forM {α : Type u} {β : Type v} {cmp : ααOrdering} {m : Type u_1Type u_2} [inst : Monad m] (f : αβm PUnit) (t : Std.RBMap α β cmp) :
Equations
@[inline]
def Std.RBMap.forIn {α : Type u} {β : Type v} {σ : Type w} {cmp : ααOrdering} {m : Type wType u_1} [inst : Monad m] (t : Std.RBMap α β cmp) (init : σ) (f : α × βσm (ForInStep σ)) :
m σ
Equations
instance Std.RBMap.instForInRBMapProd {α : Type u} {β : Type v} {cmp : ααOrdering} {m : Type u_1Type u_2} :
ForIn m (Std.RBMap α β cmp) (α × β)
Equations
  • Std.RBMap.instForInRBMapProd = { forIn := fun {β} [Monad m] => Std.RBMap.forIn }
@[inline]
def Std.RBMap.isEmpty {α : Type u} {β : Type v} {cmp : ααOrdering} :
Std.RBMap α β cmpBool
Equations
@[specialize]
def Std.RBMap.toList {α : Type u} {β : Type v} {cmp : ααOrdering} :
Std.RBMap α β cmpList (α × β)
Equations
@[inline]
def Std.RBMap.min {α : Type u} {β : Type v} {cmp : ααOrdering} :
Std.RBMap α β cmpOption (α × β)
Equations
@[inline]
def Std.RBMap.max {α : Type u} {β : Type v} {cmp : ααOrdering} :
Std.RBMap α β cmpOption (α × β)
Equations
instance Std.RBMap.instReprRBMap {α : Type u} {β : Type v} {cmp : ααOrdering} [inst : Repr α] [inst : Repr β] :
Repr (Std.RBMap α β cmp)
Equations
@[inline]
def Std.RBMap.insert {α : Type u} {β : Type v} {cmp : ααOrdering} :
Std.RBMap α β cmpαβStd.RBMap α β cmp
Equations
@[inline]
def Std.RBMap.erase {α : Type u} {β : Type v} {cmp : ααOrdering} :
Std.RBMap α β cmpαStd.RBMap α β cmp
Equations
@[specialize]
def Std.RBMap.ofList {α : Type u} {β : Type v} {cmp : ααOrdering} :
List (α × β)Std.RBMap α β cmp
Equations
@[inline]
def Std.RBMap.findCore? {α : Type u} {β : Type v} {cmp : ααOrdering} :
Std.RBMap α β cmpαOption ((_ : α) × β)
Equations
@[inline]
def Std.RBMap.find? {α : Type u} {β : Type v} {cmp : ααOrdering} :
Std.RBMap α β cmpαOption β
Equations
@[inline]
def Std.RBMap.findD {α : Type u} {β : Type v} {cmp : ααOrdering} (t : Std.RBMap α β cmp) (k : α) (v₀ : β) :
β
Equations
@[inline]
def Std.RBMap.lowerBound {α : Type u} {β : Type v} {cmp : ααOrdering} :
Std.RBMap α β cmpαOption ((_ : α) × β)
Equations
@[inline]
def Std.RBMap.contains {α : Type u} {β : Type v} {cmp : ααOrdering} (t : Std.RBMap α β cmp) (a : α) :
Equations
@[inline]
def Std.RBMap.fromList {α : Type u} {β : Type v} (l : List (α × β)) (cmp : ααOrdering) :
Std.RBMap α β cmp
Equations
@[inline]
def Std.RBMap.all {α : Type u} {β : Type v} {cmp : ααOrdering} :
Std.RBMap α β cmp(αβBool) → Bool
Equations
@[inline]
def Std.RBMap.any {α : Type u} {β : Type v} {cmp : ααOrdering} :
Std.RBMap α β cmp(αβBool) → Bool
Equations
def Std.RBMap.size {α : Type u} {β : Type v} {cmp : ααOrdering} (m : Std.RBMap α β cmp) :
Equations
def Std.RBMap.maxDepth {α : Type u} {β : Type v} {cmp : ααOrdering} (t : Std.RBMap α β cmp) :
Equations
@[inline]
def Std.RBMap.min! {α : Type u} {β : Type v} {cmp : ααOrdering} [inst : Inhabited α] [inst : Inhabited β] (t : Std.RBMap α β cmp) :
α × β
Equations
@[inline]
def Std.RBMap.max! {α : Type u} {β : Type v} {cmp : ααOrdering} [inst : Inhabited α] [inst : Inhabited β] (t : Std.RBMap α β cmp) :
α × β
Equations
@[inline]
def Std.RBMap.find! {α : Type u} {β : Type v} {cmp : ααOrdering} [inst : Inhabited β] (t : Std.RBMap α β cmp) (k : α) :
β
Equations
def Std.rbmapOf {α : Type u} {β : Type v} (l : List (α × β)) (cmp : ααOrdering) :
Std.RBMap α β cmp
Equations