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} : RBArray α β cmp

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

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

@[inline]

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

@[inline]

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

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

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

@[inline]

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

@[inline]

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

@[inline]

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

@[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 : RBArray α β cmp) : m σ

@[inline]

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

@[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 : RBArray α β cmp) : m σ

@[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 : RBArray α β cmp) : m PUnit

@[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 : RBArray α β cmp) (init : σ) (f : β → σ → m (ForInStep σ)) : m σ

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

@[inline]

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