source
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 a `Std.TreeMap` key-value index for the key `α`.
- As a `Std.TreeMap` that preserves insertion order, but is optimized for iteration-by-values. Thus, it does not store the order of keys.

- toTreeMap : Std.TreeMap α β cmp
- toArray : Array β

Instances For

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

- Lake.RBArray.empty = { toTreeMap := Std.TreeMap.empty, toArray := #[] }

Instances For

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

- Lake.RBArray.mkEmpty size = { toTreeMap := Std.TreeMap.empty, toArray := Array.mkEmpty size }

Instances For

source
@[inline]
def Lake.RBArray.find? {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} (self : RBArray α β cmp) (a : α) :
Option β
Equations

- self.find? a = self.toTreeMap.get? a

Instances For

source
@[inline]
def Lake.RBArray.contains {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} (self : RBArray α β cmp) (a : α) :
Bool
Equations

- self.contains a = self.toTreeMap.contains a

Instances For

source
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.

Equations

- self.insert a b = if self.toTreeMap.contains a = true then self else { toTreeMap := self.toTreeMap.insert a b, toArray := self.toArray.push b }

Instances For

source
@[inline]
def Lake.RBArray.all {β : Type u_1} {α : Type u_2} {cmp : α → α → Ordering} (f : β → Bool) (self : RBArray α β cmp) :
Bool
Equations

- Lake.RBArray.all f self = self.toArray.all f

Instances For

source
@[inline]
def Lake.RBArray.any {β : Type u_1} {α : Type u_2} {cmp : α → α → Ordering} (f : β → Bool) (self : RBArray α β cmp) :
Bool
Equations

- Lake.RBArray.any f self = self.toArray.any f

Instances For

source
@[inline]
def Lake.RBArray.foldl {σ : Type u_1} {β : Type u_2} {α : Type u_3} {cmp : α → α → Ordering} (f : σ → β → σ) (init : σ) (self : RBArray α β cmp) :
σ
Equations

- Lake.RBArray.foldl f init self = Array.foldl f init self.toArray

Instances For

source
@[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 σ
Equations

- Lake.RBArray.foldlM f init self = Array.foldlM f init self.toArray

Instances For

source
@[inline]
def Lake.RBArray.foldr {β : Type u_1} {σ : Type u_2} {α : Type u_3} {cmp : α → α → Ordering} (f : β → σ → σ) (init : σ) (self : RBArray α β cmp) :
σ
Equations

- Lake.RBArray.foldr f init self = Array.foldr f init self.toArray

Instances For

source
@[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 σ
Equations

- Lake.RBArray.foldrM f init self = Array.foldrM f init self.toArray

Instances For

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

- Lake.RBArray.forM f self = Array.forM f self.toArray

Instances For

source
@[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 σ
Equations

- self.forIn init f = forIn self.toArray init f

Instances For

source
@[inline]
def Lake.mkRBArray {β : Type u_1} {α : Type u_2} {cmp : α → α → Ordering} (f : β → α) (vs : Array β) :
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

Instances For