# Documentation

Lean.Attributes

@[inline]
abbrev Lean.AttrM (α : Type) :
Equations
Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations

You can tag attributes with the 'local' or 'scoped' kind. For example: attribute [local myattr, scoped yourattr, theirattr].

This is used to indicate how an attribute should be scoped.

• local means that the attribute should only be applied in the current scope and forgotten once the current section, namespace, or file is closed.
• scoped means that the attribute should only be applied while the namespace is open.
• global means that the attribute should always be applied.

Note that the attribute handler (AttributeImpl.add) is responsible for interpreting the kind and making sure that these kinds are respected.

Instances For
Equations
Equations
• One or more equations did not get rendered due to their size.
structure Lean.AttributeImplextends :
• This is run when the attribute is applied to a declaration decl. stx is the syntax of the attribute including arguments.

• erase :
Instances For
Equations

Low level attribute registration function.

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

Helper methods for decoding the parameters of builtin attributes that are defined before Lean.Parser. We have the following ones:

@[builtin_attr_parser] def simple     := leading_parser ident >> optional ident >> optional priorityParser
/- We can't use simple for class, instance, export and macro because they are  keywords. -/
@[builtin_attr_parser] def «class»    := leading_parser "class"
@[builtin_attr_parser] def «instance» := leading_parser "instance" >> optional priorityParser
@[builtin_attr_parser] def «macro»    := leading_parser "macro " >> ident


Note that we need the parsers for class, instance, and macros because they are keywords.

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

Tag attributes are simple and efficient. They are useful for marking declarations in the modules where they were defined.

The startup cost for this kind of attribute is very small since addImportedFn is a constant function.

They provide the predicate tagAttr.hasTag env decl which returns true iff declaration decl is tagged in the environment env.

Instances For
Equations
def Lean.registerTagAttribute (name : Lean.Name) (descr : String) (validate : optParam () fun x => ) (ref : ) (applicationTime : ) :
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.

A TagAttribute variant where we can attach parameters to attributes. It is slightly more expensive and consumes a little bit more memory than TagAttribute.

They provide the function pAttr.getParam env decl which returns some p iff declaration decl contains the attribute pAttr with parameter p.

Instances For
Equations
• Lean.instInhabitedParametricAttribute = { default := { attr := default, ext := default } }
structure Lean.ParametricAttributeImpl (α : Type) extends :
• This is used as the target for go-to-definition queries for simple attributes

getParam :
• afterSet : Lean.Name
• afterImport : Array (Array ())
Instances For
def Lean.registerParametricAttribute {α : Type} [inst : ] (impl : ) :
Equations
• One or more equations did not get rendered due to their size.
def Lean.ParametricAttribute.getParam? {α : Type} [inst : ] (attr : ) (env : Lean.Environment) (decl : Lean.Name) :
Equations
• One or more equations did not get rendered due to their size.
def Lean.ParametricAttribute.setParam {α : Type} (attr : ) (env : Lean.Environment) (decl : Lean.Name) (param : α) :
Equations
• One or more equations did not get rendered due to their size.
structure Lean.EnumAttributes (α : Type) :

Given a list [a₁, ..., a_n] of elements of type α, EnumAttributes provides an attribute Attr_i for associating a value a_i with an declaration. α is usually an enumeration type. Note that whenever we register an EnumAttributes, we create n attributes, but only one environment extension.

Instances For
Equations
• Lean.instInhabitedEnumAttributes = { default := { attrs := default, ext := default } }
def Lean.registerEnumAttributes {α : Type} [inst : ] (attrDescrs : List ()) (validate : optParam (Lean.Name) fun x x => ) (applicationTime : ) (ref : ) :
Equations
• One or more equations did not get rendered due to their size.
def Lean.EnumAttributes.getValue {α : Type} [inst : ] (attr : ) (env : Lean.Environment) (decl : Lean.Name) :
Equations
• One or more equations did not get rendered due to their size.
def Lean.EnumAttributes.setValue {α : Type} (attrs : ) (env : Lean.Environment) (decl : Lean.Name) (val : α) :
Equations
• One or more equations did not get rendered due to their size.

Attribute extension and builders. We use builders to implement attribute factories for parser categories.

@[inline]
Equations
@[inline]
Equations
Equations
• One or more equations did not get rendered due to their size.
def Lean.mkAttributeImplOfBuilder (builderId : Lean.Name) (ref : Lean.Name) (args : ) :
Equations
• One or more equations did not get rendered due to their size.
• decl:
• builder:
Instances For
• newEntries :
Instances For
Equations
Equations
• One or more equations did not get rendered due to their size.
@[implemented_by Lean.mkAttributeImplOfConstantUnsafe]
Equations
• One or more equations did not get rendered due to their size.
@[export lean_is_attribute]

Return true iff n is the name of a registered attribute.

Equations
• = do let m ←

Return the name of all registered attributes.

Equations
Equations
• One or more equations did not get rendered due to their size.
@[export lean_attribute_application_time]
Equations
• = do let attr ← pure attr.toAttributeImplCore.applicationTime
Equations
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
def Lean.registerAttributeOfBuilder (env : Lean.Environment) (builderId : Lean.Name) (ref : Lean.Name) (args : ) :
Equations
• One or more equations did not get rendered due to their size.
def Lean.Attribute.add (declName : Lean.Name) (attrName : Lean.Name) (stx : Lean.Syntax) :
Equations
def Lean.Attribute.erase (declName : Lean.Name) (attrName : Lean.Name) :
Equations
@[export lean_update_env_attributes]

updateEnvAttributes implementation

Equations
• One or more equations did not get rendered due to their size.
@[export lean_get_num_attributes]

getNumBuiltinAttributes implementation

Equations