ink

def Lean.NameMapExtension (α : Type) : Type

Maps declaration names to α.

Equations

• Lean.NameMapExtension α = Lean.SimplePersistentEnvExtension (Lean.Name × α) (Lean.NameMap α)

ink

instance Lean.instInhabitedNameMapExtension {α : Type} : Inhabited (Lean.NameMapExtension α)

Equations

• Lean.instInhabitedNameMapExtension = inferInstanceAs (Inhabited (Lean.SimplePersistentEnvExtension (Lean.Name × α) (Lean.NameMap α)))

ink

def Lean.NameMapExtension.find? {α : Type} (ext : Lean.NameMapExtension α) (env : Lean.Environment) : Lean.Name → Option α

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

Equations

• Lean.NameMapExtension.find? ext env = Lean.NameMap.find? (Lean.SimplePersistentEnvExtension.getState ext env)

ink

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.

ink

def Lean.registerNameMapExtension (α : Type) (name : autoParam Lean.Name _auto✝) : IO (Lean.NameMapExtension α)

Registers a new extension with the given name and type.

Equations

• One or more equations did not get rendered due to their size.

ink

structure Lean.NameMapAttributeImpl (α : Type) : Type

• The name of the attribute

  name : Lean.Name

• The declaration which creates the attribute

  ref : autoParam Lean.Name _auto✝

• 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.

  add : Lean.Name → Lean.Syntax → Lean.AttrM α

The inputs to registerNameMapAttribute.

ink

instance Lean.instInhabitedNameMapAttributeImpl : {a : Type} → Inhabited (Lean.NameMapAttributeImpl a)

Equations

• Lean.instInhabitedNameMapAttributeImpl = { default := Lean.NameMapAttributeImpl.mk default default default }

ink

def Lean.registerNameMapAttribute {α : Type} (impl : Lean.NameMapAttributeImpl α) : IO (Lean.NameMapExtension α)

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.