Maps declaration names to α.

Instances For

    Look up a value in the given extension in the environment.

    Instances For
      def Lean.NameMapExtension.add {M : TypeType} {α : Type} [Monad M] [Lean.MonadEnv M] [Lean.MonadError M] (ext : Lean.NameMapExtension α) (k : Lean.Name) (v : α) :

      Add the given k,v pair to the NameMapExtension.

      Instances For

        Registers a new extension with the given name and type.

        Instances For
          • name : Lean.Name

            The name of the attribute

          • ref : Lean.Name

            The declaration which creates the attribute

          • descr : String

            The description of the attribute

          • This function is called when the attribute is applied. It should produce a value of type α from the given attribute syntax.

          The inputs to registerNameMapAttribute.

          Instances For

            Similar to registerParametricAttribute except that attributes do not have to be assigned in the same file as the declaration.

            Instances For