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.

• toRBMap : Lean.RBMap α β cmp
• toArray : Array β

def Lake.RBArray.empty {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} : Lake.RBArray α β cmp

Equations

• Lake.RBArray.empty = { toRBMap := Lean.RBMap.empty, toArray := #[] }

instance Lake.RBArray.instEmptyCollectionRBArray {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} : EmptyCollection (Lake.RBArray α β cmp)

Equations

• Lake.RBArray.instEmptyCollectionRBArray = { emptyCollection := Lake.RBArray.empty }

def Lake.RBArray.mkEmpty {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} (size : Nat) : Lake.RBArray α β cmp

Equations

• Lake.RBArray.mkEmpty size = { toRBMap := Lean.RBMap.empty, toArray := Array.mkEmpty size }

@[inline]

def Lake.RBArray.find? {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} (self : Lake.RBArray α β cmp) (a : α) : Option β

Equations

• Lake.RBArray.find? self a = Lean.RBMap.find? self.toRBMap a

@[inline]

def Lake.RBArray.contains {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} (self : Lake.RBArray α β cmp) (a : α) : Bool

Equations

• Lake.RBArray.contains self a = Lean.RBMap.contains self.toRBMap a

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

• Lake.RBArray.insert self a b = if Lean.RBMap.contains self.toRBMap a = true then self else { toRBMap := Lean.RBMap.insert self.toRBMap a b, toArray := Array.push self.toArray b }

@[inline]

def Lake.RBArray.all {β : Type u_1} {α : Type u_2} {cmp : α → α → Ordering} (f : β → Bool) (self : Lake.RBArray α β cmp) : Bool

Equations

• Lake.RBArray.all f self = Array.all self.toArray f 0

@[inline]

def Lake.RBArray.any {β : Type u_1} {α : Type u_2} {cmp : α → α → Ordering} (f : β → Bool) (self : Lake.RBArray α β cmp) : Bool

Equations

• Lake.RBArray.any f self = Array.any self.toArray f 0

@[inline]

def Lake.RBArray.foldl {σ : Type u_1} {β : Type u_2} {α : Type u_3} {cmp : α → α → Ordering} (f : σ → β → σ) (init : σ) (self : Lake.RBArray α β cmp) : σ

Equations

• Lake.RBArray.foldl f init self = Array.foldl f init self.toArray 0

@[inline]

def Lake.RBArray.foldlM {m : Type u_1 → Type u_2} {σ : Type u_1} {β : Type u_3} {α : Type u_4} {cmp : α → α → Ordering} [Monad m] (f : σ → β → m σ) (init : σ) (self : Lake.RBArray α β cmp) : m σ

Equations

• Lake.RBArray.foldlM f init self = Array.foldlM f init self.toArray 0

@[inline]

def Lake.RBArray.foldr {β : Type u_1} {σ : Type u_2} {α : Type u_3} {cmp : α → α → Ordering} (f : β → σ → σ) (init : σ) (self : Lake.RBArray α β cmp) : σ

Equations

• Lake.RBArray.foldr f init self = Array.foldr f init self.toArray (Array.size self.toArray)

@[inline]

def Lake.RBArray.foldrM {m : Type u_1 → Type u_2} {β : Type u_3} {σ : Type u_1} {α : Type u_4} {cmp : α → α → Ordering} [Monad m] (f : β → σ → m σ) (init : σ) (self : Lake.RBArray α β cmp) : m σ

Equations

• Lake.RBArray.foldrM f init self = Array.foldrM f init self.toArray (Array.size self.toArray)

@[inline]

def Lake.RBArray.forM {m : Type u_1 → Type u_2} {β : Type u_3} {α : Type u_4} {cmp : α → α → Ordering} [Monad m] (f : β → m PUnit) (self : Lake.RBArray α β cmp) : m PUnit

Equations

• Lake.RBArray.forM f self = Array.forM f self.toArray 0

@[inline]

def Lake.RBArray.forIn {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {cmp : α → α → Ordering} {σ : Type u_1} [Monad m] (self : Lake.RBArray α β cmp) (init : σ) (f : β → σ → m (ForInStep σ)) : m σ

Equations

• Lake.RBArray.forIn self init f = Array.forIn self.toArray init f

instance Lake.RBArray.instForInRBArray {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {cmp : α → α → Ordering} : ForIn m (Lake.RBArray α β cmp) β

Equations

• Lake.RBArray.instForInRBArray = { forIn := fun {β_1 : Type u_1} [Monad m] => Lake.RBArray.forIn }