Additional functions on Lean.NameMap. #

We provide NameMap.filter and NameMap.filterMap.

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

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

Instances For
    Instances For
      def Lean.NameMap.filterMap {α : Type} {β : Type} (f : Lean.NameαOption β) (m : 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.

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