Documentation

Lean.Data.NameMap

def Lean.NameMap (α : Type) :
Equations
    Instances For
      @[inline]
      def Lean.mkNameMap (α : Type) :
      Equations
        Instances For
          instance Lean.NameMap.instRepr {α : Type} [Repr α] :
          Equations
            def Lean.NameMap.insert {α : Type} (m : NameMap α) (n : Name) (a : α) :
            Equations
              Instances For
                def Lean.NameMap.contains {α : Type} (m : NameMap α) (n : Name) :
                Equations
                  Instances For
                    def Lean.NameMap.find? {α : Type} (m : NameMap α) (n : Name) :
                    Equations
                      Instances For
                        instance Lean.NameMap.instForInProdName {α : Type} {m : Type u_1 → Type u_2} :
                        ForIn m (NameMap α) (Name × α)
                        Equations
                          def Lean.NameMap.filter {α : Type} (f : NameαBool) (m : NameMap α) :

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

                          Equations
                            Instances For
                              def Lean.NameMap.filterMap {α β : Type} (f : NameαOption β) (m : 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
                                Instances For
                                  Equations
                                    Instances For
                                      Equations
                                        Instances For
                                          Equations
                                            Instances For
                                              Equations
                                                Instances For
                                                  instance Lean.NameSet.instForInName {m : Type u_1 → Type u_2} :
                                                  Equations

                                                    The union of two NameSets.

                                                    Equations
                                                      Instances For

                                                        filter f s returns the NameSet consisting of all x in s where f x returns true.

                                                        Equations
                                                          Instances For
                                                            Equations
                                                              Instances For
                                                                @[reducible, inline]
                                                                Equations
                                                                  Instances For
                                                                    @[reducible, inline]
                                                                    Equations
                                                                      Instances For
                                                                        @[reducible, inline]
                                                                        Equations
                                                                          Instances For
                                                                            Equations
                                                                              Instances For
                                                                                @[inline]
                                                                                Equations
                                                                                  Instances For
                                                                                    Equations
                                                                                      Instances For
                                                                                        Equations
                                                                                          Instances For

                                                                                            filter f s returns the NameHashSet consisting of all x in s where f x returns true.

                                                                                            Equations
                                                                                              Instances For
                                                                                                Equations
                                                                                                  Instances For
                                                                                                    Equations
                                                                                                      Instances For