inductive Lean.AttributeApplicationTime : Type

• afterTypeChecking : AttributeApplicationTime
• afterCompilation : AttributeApplicationTime
• beforeElaboration : AttributeApplicationTime

instance Lean.instInhabitedAttributeApplicationTime : Inhabited AttributeApplicationTime

instance Lean.instBEqAttributeApplicationTime : BEq AttributeApplicationTime

@[reducible, inline]

abbrev Lean.AttrM (α : Type) : Type

instance Lean.instMonadLiftImportMAttrM : MonadLift ImportM AttrM

structure Lean.AttributeImplCore : Type

• ref : Name

  This is used as the target for go-to-definition queries for simple attributes

• name : Name
• descr : String
• applicationTime : AttributeApplicationTime

instance Lean.instInhabitedAttributeImplCore : Inhabited AttributeImplCore

inductive Lean.AttributeKind : Type

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.

• global : AttributeKind
• local : AttributeKind
• scoped : AttributeKind

instance Lean.instBEqAttributeKind : BEq AttributeKind

instance Lean.instInhabitedAttributeKind : Inhabited AttributeKind

instance Lean.instToStringAttributeKind : ToString AttributeKind

structure Lean.AttributeImplextends Lean.AttributeImplCore : Type

• ref : Name
• name : Name
• descr : String
• applicationTime : AttributeApplicationTime
• add (decl : Name) (stx : Syntax) (kind : AttributeKind) : AttrM Unit

  This is run when the attribute is applied to a declaration decl. stx is the syntax of the attribute including arguments.

• erase (decl : Name) : AttrM Unit

instance Lean.instInhabitedAttributeImpl : Inhabited AttributeImpl

opaque Lean.attributeMapRef : IO.Ref (Std.HashMap Name AttributeImpl)

def Lean.registerBuiltinAttribute (attr : AttributeImpl) : IO Unit

Low level attribute registration function.

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 (ppSpace >> (priorityParser <|> ident))
@[builtin_attr_parser] def «macro»    := leading_parser "macro " >> ident
@[builtin_attr_parser] def «export»   := leading_parser "export " >> ident

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

def Lean.Attribute.Builtin.ensureNoArgs (stx : Syntax) : AttrM Unit

def Lean.Attribute.Builtin.getIdent? (stx : Syntax) : AttrM (Option Syntax)

def Lean.Attribute.Builtin.getIdent (stx : Syntax) : AttrM Syntax

def Lean.Attribute.Builtin.getId? (stx : Syntax) : AttrM (Option Name)

def Lean.Attribute.Builtin.getId (stx : Syntax) : AttrM Name

def Lean.getAttrParamOptPrio (optPrioStx : Syntax) : AttrM Nat

def Lean.Attribute.Builtin.getPrio (stx : Syntax) : AttrM Nat

structure Lean.TagAttribute : Type

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.

• attr : AttributeImpl
• ext : PersistentEnvExtension Name Name NameSet

instance Lean.instInhabitedTagAttribute : Inhabited TagAttribute

def Lean.registerTagAttribute (name : Name) (descr : String) (validate : Name → AttrM Unit := fun (x : Name) => pure ()) (ref : Name := by exact decl_name%) (applicationTime : AttributeApplicationTime := AttributeApplicationTime.afterTypeChecking) : IO TagAttribute

def Lean.TagAttribute.hasTag (attr : TagAttribute) (env : Environment) (decl : Name) : Bool

structure Lean.ParametricAttribute (α : Type) : Type

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.

• attr : AttributeImpl
• ext : PersistentEnvExtension (Name × α) (Name × α) (NameMap α)

instance Lean.instInhabitedParametricAttribute {a✝ : Type} : Inhabited (ParametricAttribute a✝)

structure Lean.ParametricAttributeImpl (α : Type) extends Lean.AttributeImplCore : Type

• ref : Name
• name : Name
• descr : String
• applicationTime : AttributeApplicationTime
• getParam : Name → Syntax → AttrM α
• afterSet : Name → α → AttrM Unit
• afterImport : Array (Array (Name × α)) → ImportM Unit

def Lean.registerParametricAttribute {α : Type} (impl : ParametricAttributeImpl α) : IO (ParametricAttribute α)

def Lean.ParametricAttribute.getParam? {α : Type} [Inhabited α] (attr : ParametricAttribute α) (env : Environment) (decl : Name) : Option α

def Lean.ParametricAttribute.setParam {α : Type} (attr : ParametricAttribute α) (env : Environment) (decl : Name) (param : α) : Except String Environment

structure Lean.EnumAttributes (α : Type) : 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.

• attrs : List AttributeImpl
• ext : PersistentEnvExtension (Name × α) (Name × α) (NameMap α)

instance Lean.instInhabitedEnumAttributes {a✝ : Type} : Inhabited (EnumAttributes a✝)

def Lean.registerEnumAttributes {α : Type} (attrDescrs : List (Name × String × α)) (validate : Name → α → AttrM Unit := fun (x : Name) (x : α) => pure ()) (applicationTime : AttributeApplicationTime := AttributeApplicationTime.afterTypeChecking) (ref : Name := by exact decl_name%) : IO (EnumAttributes α)

def Lean.EnumAttributes.getValue {α : Type} [Inhabited α] (attr : EnumAttributes α) (env : Environment) (decl : Name) : Option α

def Lean.EnumAttributes.setValue {α : Type} (attrs : EnumAttributes α) (env : Environment) (decl : Name) (val : α) : Except String Environment

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

@[reducible, inline]

abbrev Lean.AttributeImplBuilder : Type

@[reducible, inline]

abbrev Lean.AttributeImplBuilderTable : Type

opaque Lean.attributeImplBuilderTableRef : IO.Ref AttributeImplBuilderTable

def Lean.registerAttributeImplBuilder (builderId : Name) (builder : AttributeImplBuilder) : IO Unit

structure Lean.AttributeExtensionOLeanEntry : Type

• builderId : Name
• ref : Name
• args : List DataValue

def Lean.mkAttributeImplOfEntry (e : AttributeExtensionOLeanEntry) : IO AttributeImpl

structure Lean.AttributeExtensionState : Type

• newEntries : List AttributeExtensionOLeanEntry
• map : Std.HashMap Name AttributeImpl

instance Lean.instInhabitedAttributeExtensionState : Inhabited AttributeExtensionState

@[reducible, inline]

abbrev Lean.AttributeExtension : Type

unsafe def Lean.mkAttributeImplOfConstantUnsafe (env : Environment) (opts : Options) (declName : Name) : Except String AttributeImpl

@[implemented_by Lean.mkAttributeImplOfConstantUnsafe]

opaque Lean.mkAttributeImplOfConstant (env : Environment) (opts : Options) (declName : Name) : Except String AttributeImpl

opaque Lean.attributeExtension : AttributeExtension

@[export lean_is_attribute]

def Lean.isBuiltinAttribute (n : Name) : IO Bool

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

def Lean.getBuiltinAttributeNames : IO (List Name)

Return the name of all registered attributes.

def Lean.getBuiltinAttributeImpl (attrName : Name) : IO AttributeImpl

@[export lean_attribute_application_time]

def Lean.getBuiltinAttributeApplicationTime (n : Name) : IO AttributeApplicationTime

def Lean.isAttribute (env : Environment) (attrName : Name) : Bool

def Lean.getAttributeNames (env : Environment) : List Name

def Lean.getAttributeImpl (env : Environment) (attrName : Name) : Except String AttributeImpl

def Lean.registerAttributeOfBuilder (env : Environment) (builderId ref : Name) (args : List DataValue) : IO Environment

def Lean.Attribute.add (declName attrName : Name) (stx : Syntax) (kind : AttributeKind := AttributeKind.global) : AttrM Unit

def Lean.Attribute.erase (declName attrName : Name) : AttrM Unit

@[export lean_update_env_attributes]

def Lean.updateEnvAttributesImpl (env : Environment) : IO Environment

updateEnvAttributes implementation

@[export lean_get_num_attributes]

def Lean.getNumBuiltinAttributesImpl : IO Nat

getNumBuiltinAttributes implementation