Documentation

Std.Lean.NameMapAttribute

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

Equations
def Lean.NameMapExtension.add {M : TypeType} {α : Type} [inst : Monad M] [inst : Lean.MonadEnv M] [inst : Lean.MonadError M] (ext : Lean.NameMapExtension α) (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.

Registers a new extension with the given name and type.

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

The inputs to registerNameMapAttribute.

Instances For
    Equations

    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.