# Documentation

Std.Lean.NameMapAttribute

Maps declaration names to α.

Equations
Equations
• Lean.instInhabitedNameMapExtension =
def Lean.NameMapExtension.find? {α : Type} (ext : ) (env : Lean.Environment) :

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

Equations
def Lean.NameMapExtension.add {M : } {α : Type} [inst : ] [inst : ] [inst : ] (ext : ) (k : Lean.Name) (v : α) :

Add the given k,v pair to the NameMapExtension.

Equations
• One or more equations did not get rendered due to their size.
def Lean.registerNameMapExtension (α : Type) (name : ) :

Registers a new extension with the given name and type.

Equations
• One or more equations did not get rendered due to their size.
• The name of the attribute

name : Lean.Name
• The declaration which creates the attribute

ref :
• The description of the attribute

descr : String
• 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.
Similar to registerParametricAttribute except that attributes do not have to be assigned in the same file as the declaration.