Maps declaration names to α
.
Equations
Equations
- Lean.instInhabitedNameMapExtension = inferInstanceAs (Inhabited (Lean.SimplePersistentEnvExtension (Lean.Name × α) (Lean.NameMap α)))
def
Lean.NameMapExtension.find?
{α : Type}
(ext : Lean.NameMapExtension α)
(env : Lean.Environment)
:
Look up a value in the given extension in the environment.
Equations
def
Lean.NameMapExtension.add
{M : Type → Type}
{α : Type}
[inst : Monad M]
[inst : Lean.MonadEnv M]
[inst : Lean.MonadError M]
(ext : Lean.NameMapExtension α)
(k : Lean.Name)
(v : α)
:
M Unit
Add the given k,v pair to the NameMapExtension.
Equations
- One or more equations did not get rendered due to their size.
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.NameThe declaration which creates the attribute
The description of the attribute
descr : StringThis function is called when the attribute is applied. It should produce a value of type
α
from the given attribute syntax.add : Lean.Name → Lean.Syntax → Lean.AttrM α
The inputs to registerNameMapAttribute
.
Instances For
instance
Lean.instInhabitedNameMapAttributeImpl :
{a : Type} → Inhabited (Lean.NameMapAttributeImpl a)
Equations
- Lean.instInhabitedNameMapAttributeImpl = { default := Lean.NameMapAttributeImpl.mk default default default }
Similar to registerParametricAttribute
except that attributes do not
have to be assigned in the same file as the declaration.
Equations
- One or more equations did not get rendered due to their size.