Documentation

Lake.Util.RBArray

structure Lake.RBArray (α : Type u) (β : Type v) (cmp : ααOrdering) :
Type (max u v)

There are two ways to think of this type:

• As an Array of values with an RBMap key-value index for the key α.
• As an RBMap that preserves insertion order, but is optimized for iteration-by-values. Thus, it does not store the order of keys.
Instances For
def Lake.RBArray.empty {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} :
Lake.RBArray α β cmp
Equations
• Lake.RBArray.empty = { toRBMap := Lean.RBMap.empty, toArray := #[] }
Instances For
instance Lake.RBArray.instEmptyCollection {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} :
Equations
• Lake.RBArray.instEmptyCollection = { emptyCollection := Lake.RBArray.empty }
def Lake.RBArray.mkEmpty {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} (size : Nat) :
Lake.RBArray α β cmp
Equations
Instances For
@[inline]
def Lake.RBArray.find? {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} (self : Lake.RBArray α β cmp) (a : α) :
Equations
• self.find? a = self.toRBMap.find? a
Instances For
@[inline]
def Lake.RBArray.contains {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} (self : Lake.RBArray α β cmp) (a : α) :
Equations
• self.contains a = self.toRBMap.contains a
Instances For
def Lake.RBArray.insert {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} (self : Lake.RBArray α β cmp) (a : α) (b : β) :
Lake.RBArray α β cmp

Insert b with the key a. Does nothing if the key is already present.

Equations
• self.insert a b = if self.toRBMap.contains a = true then self else { toRBMap := self.toRBMap.insert a b, toArray := self.toArray.push b }
Instances For
@[inline]
def Lake.RBArray.all {β : Type u_1} {α : Type u_2} {cmp : ααOrdering} (f : βBool) (self : Lake.RBArray α β cmp) :
Equations
Instances For
@[inline]
def Lake.RBArray.any {β : Type u_1} {α : Type u_2} {cmp : ααOrdering} (f : βBool) (self : Lake.RBArray α β cmp) :
Equations
Instances For
@[inline]
def Lake.RBArray.foldl {σ : Type u_1} {β : Type u_2} {α : Type u_3} {cmp : ααOrdering} (f : σβσ) (init : σ) (self : Lake.RBArray α β cmp) :
σ
Equations
Instances For
@[inline]
def Lake.RBArray.foldlM {m : Type u_1 → Type u_2} {σ : Type u_1} {β : Type u_3} {α : Type u_4} {cmp : ααOrdering} [] (f : σβm σ) (init : σ) (self : Lake.RBArray α β cmp) :
m σ
Equations
Instances For
@[inline]
def Lake.RBArray.foldr {β : Type u_1} {σ : Type u_2} {α : Type u_3} {cmp : ααOrdering} (f : βσσ) (init : σ) (self : Lake.RBArray α β cmp) :
σ
Equations
Instances For
@[inline]
def Lake.RBArray.foldrM {m : Type u_1 → Type u_2} {β : Type u_3} {σ : Type u_1} {α : Type u_4} {cmp : ααOrdering} [] (f : βσm σ) (init : σ) (self : Lake.RBArray α β cmp) :
m σ
Equations
Instances For
@[inline]
def Lake.RBArray.forM {m : Type u_1 → Type u_2} {β : Type u_3} {α : Type u_4} {cmp : ααOrdering} [] (f : β) (self : Lake.RBArray α β cmp) :
Equations
Instances For
@[inline]
def Lake.RBArray.forIn {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {cmp : ααOrdering} {σ : Type u_1} [] (self : Lake.RBArray α β cmp) (init : σ) (f : βσm ()) :
m σ
Equations
• self.forIn init f = self.toArray.forIn init f
Instances For
instance Lake.RBArray.instForIn {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {cmp : ααOrdering} :
ForIn m (Lake.RBArray α β cmp) β
Equations
• Lake.RBArray.instForIn = { forIn := fun {β_1 : Type u_1} [] => Lake.RBArray.forIn }
@[inline]
def Lake.mkRBArray {β : Type u_1} {α : Type u_2} {cmp : ααOrdering} (f : βα) (vs : ) :
Lake.RBArray α β cmp
Equations
Instances For