Red-Black Dictionary

Defines an insertion-ordered key-value mapping backed by an red-black tree. Implemented via a key-index RBMap into an Array of key-value pairs.

structure Lake.Toml.RBDict (α : Type u) (β : Type v) (cmp : α → α → Ordering) : Type (max u v)

• items : Array (α × β)
• indices : Lean.RBMap α Nat cmp

instance Lake.Toml.instInhabitedRBDict {a✝ : Type u_1} {a✝¹ : Type u_2} {a✝² : a✝ → a✝ → Ordering} : Inhabited (RBDict a✝ a✝¹ a✝²)

@[reducible, inline]

abbrev Lake.Toml.NameDict (α : Type u) : Type u

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

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

def Lake.Toml.RBDict.mkEmpty {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} (capacity : Nat) : RBDict α β cmp

def Lake.Toml.RBDict.ofArray {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} (items : Array (α × β)) : RBDict α β cmp

def Lake.Toml.RBDict.beq {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} [BEq (α × β)] (self other : RBDict α β cmp) : Bool

instance Lake.Toml.RBDict.instBEqOfProd {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} [BEq (α × β)] : BEq (RBDict α β cmp)

@[reducible, inline]

abbrev Lake.Toml.RBDict.size {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} (t : RBDict α β cmp) : Nat

@[reducible, inline]

abbrev Lake.Toml.RBDict.isEmpty {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} (t : RBDict α β cmp) : Bool

def Lake.Toml.RBDict.keys {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} (t : RBDict α β cmp) : Array α

def Lake.Toml.RBDict.values {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} (t : RBDict α β cmp) : Array β

def Lake.Toml.RBDict.contains {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} (k : α) (t : RBDict α β cmp) : Bool

def Lake.Toml.RBDict.findIdx? {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} (k : α) (t : RBDict α β cmp) : Option (Fin t.size)

def Lake.Toml.RBDict.findEntry? {α β : Type} {cmp : α → α → Ordering} (k : α) (t : RBDict α β cmp) : Option (α × β)

@[inline]

def Lake.Toml.RBDict.find? {α β : Type} {cmp : α → α → Ordering} (k : α) (t : RBDict α β cmp) : Option β

def Lake.Toml.RBDict.push {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} (k : α) (v : β) (t : RBDict α β cmp) : RBDict α β cmp

@[specialize #[]]

def Lake.Toml.RBDict.alter {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} (k : α) (f : Option β → β) (t : RBDict α β cmp) : RBDict α β cmp

def Lake.Toml.RBDict.insert {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} (k : α) (v : β) (t : RBDict α β cmp) : RBDict α β cmp

@[macro_inline]

def Lake.Toml.RBDict.insertIf {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} (p : Bool) (k : α) (v : β) (t : RBDict α β cmp) : RBDict α β cmp

Inserts the value into the dictionary if p is true.

@[macro_inline]

def Lake.Toml.RBDict.insertUnless {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} (p : Bool) (k : α) (v : β) (t : RBDict α β cmp) : RBDict α β cmp

Inserts the value into the dictionary if p is false.

@[macro_inline]

def Lake.Toml.RBDict.insertSome {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} (k : α) (v? : Option β) (t : RBDict α β cmp) : RBDict α β cmp

Insert the value into the dictionary if it is not none.

def Lake.Toml.RBDict.appendArray {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} (self : RBDict α β cmp) (other : Array (α × β)) : RBDict α β cmp

instance Lake.Toml.RBDict.instHAppendArrayProd {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} : HAppend (RBDict α β cmp) (Array (α × β)) (RBDict α β cmp)

@[inline]

def Lake.Toml.RBDict.append {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} (self other : RBDict α β cmp) : RBDict α β cmp

instance Lake.Toml.RBDict.instAppend {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} : Append (RBDict α β cmp)

@[inline]

def Lake.Toml.RBDict.map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {cmp : α → α → Ordering} (f : α → β → γ) (t : RBDict α β cmp) : RBDict α γ cmp

@[inline]

def Lake.Toml.RBDict.filter {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} (p : α → β → Bool) (t : RBDict α β cmp) : RBDict α β cmp

@[inline]

def Lake.Toml.RBDict.filterMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {cmp : α → α → Ordering} (f : α → β → Option γ) (t : RBDict α β cmp) : RBDict α γ cmp

@[inline]

def Lake.Toml.RBDict.foldM {m : Type u_1 → Type u_2} {σ : Type u_1} {α : Type u_3} {β : Type u_4} {cmp : α → α → Ordering} [Monad m] (f : σ → α → β → m σ) (init : σ) (t : RBDict α β cmp) : m σ

@[inline]

def Lake.Toml.RBDict.fold {σ : Type u_1} {α : Type u_2} {β : Type u_3} {cmp : α → α → Ordering} (f : σ → α → β → σ) (init : σ) (t : RBDict α β cmp) : σ