RBMap (Red-Black Map)🔗

RBMap is a persistent, ordered map. It is often preferred in pure functional code because it doesn't rely on the IO or ST monads for performance.

def Lean.RBMap.{u, v} : (α : Type u) → Type v → (α → α → Ordering) → Type (max u v) :=
fun α β cmp => { t // RBNode.WellFormed cmp t }#print RBMap
def myRBMap : RBMap Name Nat Name.quickCmp := {}

-- Inserting values
def rb1 := myRBMap.insert `apple 1
def rb2 := rb1.insert `banana 2

-- Accessing values (returns Option)
some 1#eval rb2.find? `apple
none#eval rb2.find? `cherry 

-- Checking for existence
true#eval rb2.contains "apple".toName
false#eval rb2.contains `cherry

-- Converting to list
[(`banana, 2), (`apple, 1)]#eval rb2.toList
[("banana", 20), ("apple", 10)]#eval rb2.toList.map (λ (k, v) => (k.toString, v * 10))