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 β

Instances For

• Lake.RBArray.instEmptyCollection
• Lake.RBArray.instForIn

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.instEmptyCollection {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} : EmptyCollection (Lake.RBArray α β cmp)

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

• 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

• self.find? a = self.toRBMap.find? a

@[inline]

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

Equations

• self.contains a = self.toRBMap.contains 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

• self.insert a b = if self.toRBMap.contains a = true then self else { toRBMap := self.toRBMap.insert a b, toArray := self.toArray.push 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 = self.toArray.all f

@[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 = self.toArray.any f

@[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

@[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

@[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

@[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

@[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

@[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

• self.forIn init f = forIn self.toArray init f

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.37} [Monad m] => Lake.RBArray.forIn }

@[inline]

def Lake.mkRBArray {β : Type u_1} {α : Type u_2} {cmp : α → α → Ordering} (f : β → α) (vs : Array β) : Lake.RBArray α β cmp

Equations

• Lake.mkRBArray f vs = Array.foldl (fun (m : Lake.RBArray α β cmp) (v : β) => m.insert (f v) v) (Lake.RBArray.mkEmpty vs.size) vs