inductive Lean.AttributeApplicationTime : Type

• afterTypeChecking: Lean.AttributeApplicationTime
• afterCompilation: Lean.AttributeApplicationTime
• beforeElaboration: Lean.AttributeApplicationTime

instance Lean.instInhabitedAttributeApplicationTime : Inhabited Lean.AttributeApplicationTime

instance Lean.instBEqAttributeApplicationTime : BEq Lean.AttributeApplicationTime

@[inline, reducible]

abbrev Lean.AttrM (α : Type) : Type

instance Lean.instMonadLiftImportMAttrM : MonadLift Lean.ImportM Lean.AttrM

structure Lean.AttributeImplCore : Type

• ref : Lake.Name

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

• name : Lake.Name
• descr : String
• applicationTime : Lean.AttributeApplicationTime

instance Lean.instInhabitedAttributeImplCore : Inhabited Lean.AttributeImplCore

inductive Lean.AttributeKind : Type

• global: Lean.AttributeKind
• local: Lean.AttributeKind
• scoped: Lean.AttributeKind

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.

instance Lean.instBEqAttributeKind : BEq Lean.AttributeKind

instance Lean.instInhabitedAttributeKind : Inhabited Lean.AttributeKind

instance Lean.instToStringAttributeKind : ToString Lean.AttributeKind

structure Lean.AttributeImplextends Lean.AttributeImplCore : Type

• ref : Lake.Name
• name : Lake.Name
• descr : String
• applicationTime : Lean.AttributeApplicationTime
• add : Lake.Name → Lean.Syntax → Lean.AttributeKind → Lean.AttrM Unit

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

• erase : Lake.Name → Lean.AttrM Unit

instance Lean.instInhabitedAttributeImpl : Inhabited Lean.AttributeImpl

opaque Lean.attributeMapRef : IO.Ref (Lean.PersistentHashMap Lake.Name Lean.AttributeImpl)

def Lean.registerBuiltinAttribute (attr : Lean.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 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.

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

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

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

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

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

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

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

structure Lean.TagAttribute : Type

• attr : Lean.AttributeImpl
• ext : Lean.PersistentEnvExtension Lake.Name Lake.Name Lean.NameSet

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.

instance Lean.instInhabitedTagAttribute : Inhabited Lean.TagAttribute

def Lean.registerTagAttribute (name : Lake.Name) (descr : String) (validate : optParam (Lake.Name → Lean.AttrM Unit) fun x => pure ()) (ref : autoParam Lake.Name _auto✝) (applicationTime : optParam Lean.AttributeApplicationTime Lean.AttributeApplicationTime.afterTypeChecking) : IO Lean.TagAttribute

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

structure Lean.ParametricAttribute (α : Type) : Type

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

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.

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

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

• ref : Lake.Name
• name : Lake.Name
• descr : String
• applicationTime : Lean.AttributeApplicationTime
• getParam : Lake.Name → Lean.Syntax → Lean.AttrM α

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

• afterSet : Lake.Name → α → Lean.AttrM Unit
• afterImport : Array (Array (Lake.Name × α)) → Lean.ImportM Unit

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

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

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

structure Lean.EnumAttributes (α : Type) : Type

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

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.

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

def Lean.registerEnumAttributes {α : Type} [Inhabited α] (attrDescrs : List (Lake.Name × String × α)) (validate : optParam (Lake.Name → α → Lean.AttrM Unit) fun x x => pure ()) (applicationTime : optParam Lean.AttributeApplicationTime Lean.AttributeApplicationTime.afterTypeChecking) (ref : autoParam Lake.Name _auto✝) : IO (Lean.EnumAttributes α)

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

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

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

@[inline, reducible]

abbrev Lean.AttributeImplBuilder : Type

@[inline, reducible]

abbrev Lean.AttributeImplBuilderTable : Type

opaque Lean.attributeImplBuilderTableRef : IO.Ref Lean.AttributeImplBuilderTable

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

def Lean.mkAttributeImplOfBuilder (builderId : Lake.Name) (ref : Lake.Name) (args : List Lean.DataValue) : IO Lean.AttributeImpl

inductive Lean.AttributeExtensionOLeanEntry : Type

• decl: Lake.Name → Lean.AttributeExtensionOLeanEntry
• builder: Lake.Name → Lake.Name → List Lean.DataValue → Lean.AttributeExtensionOLeanEntry

structure Lean.AttributeExtensionState : Type

• newEntries : List Lean.AttributeExtensionOLeanEntry
• map : Lean.PersistentHashMap Lake.Name Lean.AttributeImpl

instance Lean.instInhabitedAttributeExtensionState : Inhabited Lean.AttributeExtensionState

@[inline, reducible]

abbrev Lean.AttributeExtension : Type

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

@[implemented_by Lean.mkAttributeImplOfConstantUnsafe]

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

def Lean.mkAttributeImplOfEntry (env : Lean.Environment) (opts : Lean.Options) (e : Lean.AttributeExtensionOLeanEntry) : IO Lean.AttributeImpl

opaque Lean.attributeExtension : Lean.AttributeExtension

@[export lean_is_attribute]

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

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

def Lean.getBuiltinAttributeNames : IO (List Lake.Name)

Return the name of all registered attributes.

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

@[export lean_attribute_application_time]

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

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

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

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

def Lean.registerAttributeOfDecl (env : Lean.Environment) (opts : Lean.Options) (attrDeclName : Lake.Name) : Except String Lean.Environment

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

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

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

@[export lean_update_env_attributes]

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

updateEnvAttributes implementation

@[export lean_get_num_attributes]

def Lean.getNumBuiltinAttributesImpl : IO Nat

getNumBuiltinAttributes implementation