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

filterMap f m filters an NameMap and simultaneously modifies 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 = Std.TreeMap.filterMap f m