Additional functions on Lean.NameMap.

We provide NameMap.filter and NameMap.filterMap.

instance Lean.NameMap.instForInProdName_batteries {m : Type u_1 → Type u_2} {β : Type} : ForIn m (Lean.NameMap β) (Lean.Name × β)

Equations

• Lean.NameMap.instForInProdName_batteries = inferInstanceAs (ForIn m (Lean.RBMap Lean.Name β Lean.Name.quickCmp) (Lean.Name × β))

def Lean.NameMap.filter {α : Type} (f : Lean.Name → α → Bool) (m : Lean.NameMap α) : Lean.NameMap α

filter f m returns the NameMap consisting of all "key/val"-pairs in m where f key val returns true.

Equations

• Lean.NameMap.filter f m = Lean.RBMap.fold (Lean.NameMap.filter.process f) ∅ m

def Lean.NameMap.filter.process {α : Type} (f : Lean.Name → α → Bool) (r : Lean.NameMap α) (n : Lean.Name) (i : α) : Lean.RBMap Lean.Name α Lean.Name.quickCmp

see Lean.NameMap.filter

Equations

• Lean.NameMap.filter.process f r n i = if f n i = true then r.insert n i else r

def Lean.NameMap.filterMap {α β : Type} (f : Lean.Name → α → Option β) (m : Lean.NameMap α) : Lean.NameMap β

filterMap f m allows to filter a NameMap and simultaneously modify the filtered values.

It takes a function f : Name → α → Option β and applies f name to the value with key name. The resulting entries with non-none value are collected to form the output NameMap.

Equations

• Lean.NameMap.filterMap f m = Lean.RBMap.fold (Lean.NameMap.filterMap.process f) ∅ m

def Lean.NameMap.filterMap.process {α β : Type} (f : Lean.Name → α → Option β) (r : Lean.NameMap β) (n : Lean.Name) (i : α) : Lean.NameMap β

see Lean.NameMap.filterMap

Equations

• Lean.NameMap.filterMap.process f r n i = match f n i with | none => r | some b => r.insert n b