Documentation

Mathlib.Lean.Data.NameMap

Additional functions on Lean.NameMap. #

We provide NameMap.filter and NameMap.filterMap.

instance Lean.NameMap.instForInNameMapProdName_1 {m : Type u_1 → Type u_2} {β : Type} :
Equations
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.

Equations
Instances For
    Equations
    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.

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