Attributes are an extensible set of compile-time annotations on declarations.
They can be added as a declaration modifier or using the Lean.Parser.Command.attribute : commandattribute command.
Attributes can associate information with declarations in compile-time tables (including custom simp sets, macros, and instances), impose additional requirements on definitions (e.g. rejecting them if their type is not a type class), or generate additional code.
As with macros and custom elaborators for terms, commands, and tactics, the syntax category attr of attributes is designed to be extended, and there is a table that maps each extension to a compile-time program that interprets it.
Attributes are applied as attribute instances that pair a scope indicator with an attribute.
These may occur either in attributes as declaration modifiers or the stand-alone Lean.Parser.Command.attribute : commandattribute command.
attrInstance ::= ...
| `attrKind` matches `("scoped" <|> "local")?`, used before an attribute like `@[local simp]`.
An attrKind is the optional attribute scope keywords local or scoped.
These control the visibility of the attribute's effects.
The attribute itself is anything from the extensible syntax category attr.
The attribute system is very powerful: attributes can associate arbitrary information with declarations and generate any number of helpers. This imposes some design trade-offs: storing this information takes space, and retrieving it takes time. As a result, some attributes can only be applied to a declaration in the module where the declaration is defined. This allows lookups to be much faster in large projects, because they don't need to examine data for all modules. Each attribute determines how to store its own metadata and what the appropriate tradeoff between flexibility and performance is for a given use case.
Attributes can be added to declarations as a declaration modifier. They are placed between the documentation comment and the visibility modifiers.
attribute Command
The Lean.Parser.Command.attribute : commandattribute command can be used to modify a declaration's attributes.
Some example uses include:
registering a pre-existing declaration as an instance in the local scope by adding instance,
marking a pre-existing theorem as a simp lemma or an extensionality lemma, using simp or ext, and
temporarily removing a simp lemma from the default simp set.
The Lean.Parser.Command.attribute : commandattribute command adds or removes attributes from an existing declaration.
The identifier is the name whose attributes are being modified.
command ::= ... | attribute [(eraseAttr | attrInstance),*] ident
In addition to attribute instances that add an attribute to an existing declaration, some attributes can be removed; this is called erasing the attribute.
Attributes can be erased by preceding their name with -.
Not all attributes support erasure, however.
Attributes are erased by preceding their name with a -.
eraseAttr ::= ... | -ident
Many attributes can be applied in a particular scope. This determines whether the attribute's effect is visible only in the current section scope, in namespaces that open the current namespace, or everywhere. These scope indications are also used to control syntax extensions and type class instances. Each attribute is responsible for defining precisely what these terms mean for its particular effect.
Globally-scoped declarations (the default) are in effect whenever the module in which they're established is transitively imported. They are indicated by the absence of another scope modifier.
attrKind ::=
`attrKind` matches `("scoped" <|> "local")?`, used before an attribute like `@[local simp]`. Locally-scoped declarations are in effect only for the extent of the section scope in which they are established.
attrKind ::= ...
| `attrKind` matches `("scoped" <|> "local")?`, used before an attribute like `@[local simp]`. Scoped declarations are in effect whenever the namespace in which they are established is opened.
attrKind ::= ...
| `attrKind` matches `("scoped" <|> "local")?`, used before an attribute like `@[local simp]`.