inductive Lean.AttributeApplicationTime : Type

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

instance Lean.instInhabitedAttributeApplicationTime : Inhabited Lean.AttributeApplicationTime

Equations

• Lean.instInhabitedAttributeApplicationTime = { default := Lean.AttributeApplicationTime.afterTypeChecking }

instance Lean.instBEqAttributeApplicationTime : BEq Lean.AttributeApplicationTime

Equations

• Lean.instBEqAttributeApplicationTime = { beq := Lean.beqAttributeApplicationTime✝ }

@[reducible, inline]

abbrev Lean.AttrM (α : Type) : Type

Equations

• Lean.AttrM = Lean.CoreM

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

Equations

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

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

Equations

• Lean.instInhabitedAttributeImplCore = { default := { ref := default, name := default, descr := default, applicationTime := default } }

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: Lean.AttributeKind
• local: Lean.AttributeKind
• scoped: Lean.AttributeKind

instance Lean.instBEqAttributeKind : BEq Lean.AttributeKind

Equations

• Lean.instBEqAttributeKind = { beq := Lean.beqAttributeKind✝ }

instance Lean.instInhabitedAttributeKind : Inhabited Lean.AttributeKind

Equations

• Lean.instInhabitedAttributeKind = { default := Lean.AttributeKind.global }

instance Lean.instToStringAttributeKind : ToString Lean.AttributeKind

Equations

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

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

Equations

• Lean.instInhabitedAttributeImpl = { default := { toAttributeImplCore := default, add := default, erase := default } }

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

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

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 (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 : Lean.Syntax) : Lean.AttrM Unit

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Lean.Attribute.Builtin.getId? stx = do let ident? ← Lean.Attribute.Builtin.getIdent? stx pure (Lean.Syntax.getId <$> ident?)

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

Equations

• Lean.Attribute.Builtin.getId stx = do let __do_lift ← Lean.Attribute.Builtin.getIdent stx pure __do_lift.getId

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

Equations

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

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

Equations

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

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 : Lean.AttributeImpl
• ext : Lean.PersistentEnvExtension Lake.Name Lake.Name Lean.NameSet

instance Lean.instInhabitedTagAttribute : Inhabited Lean.TagAttribute

Equations

• Lean.instInhabitedTagAttribute = { default := { attr := default, ext := default } }

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

Equations

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

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

Equations

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

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 : Lean.AttributeImpl
• ext : Lean.PersistentEnvExtension (Lake.Name × α) (Lake.Name × α) (Lake.NameMap α)

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

Equations

• Lean.instInhabitedParametricAttribute = { default := { attr := default, ext := default } }

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 α
• afterSet : Lake.Name → α → Lean.AttrM Unit
• afterImport : Array (Array (Lake.Name × α)) → Lean.ImportM Unit

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

Equations

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

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

Equations

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

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

Equations

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

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 Lean.AttributeImpl
• ext : Lean.PersistentEnvExtension (Lake.Name × α) (Lake.Name × α) (Lake.NameMap α)

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

Equations

• Lean.instInhabitedEnumAttributes = { default := { attrs := default, ext := default } }

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

Equations

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

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

Equations

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

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

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.

@[reducible, inline]

abbrev Lean.AttributeImplBuilder : Type

Equations

• Lean.AttributeImplBuilder = (Lake.Name → List Lean.DataValue → Except String Lean.AttributeImpl)

@[reducible, inline]

abbrev Lean.AttributeImplBuilderTable : Type

Equations

• Lean.AttributeImplBuilderTable = Std.HashMap Lake.Name Lean.AttributeImplBuilder

opaque Lean.attributeImplBuilderTableRef : IO.Ref Lean.AttributeImplBuilderTable

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

Equations

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

structure Lean.AttributeExtensionOLeanEntry : Type

• builderId : Lake.Name
• ref : Lake.Name
• args : List Lean.DataValue

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

Equations

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

structure Lean.AttributeExtensionState : Type

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

instance Lean.instInhabitedAttributeExtensionState : Inhabited Lean.AttributeExtensionState

Equations

• Lean.instInhabitedAttributeExtensionState = { default := { newEntries := default, map := default } }

@[reducible, inline]

abbrev Lean.AttributeExtension : Type

Equations

• Lean.AttributeExtension = Lean.PersistentEnvExtension Lean.AttributeExtensionOLeanEntry (Lean.AttributeExtensionOLeanEntry × Lean.AttributeImpl) Lean.AttributeExtensionState

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

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.

Equations

• Lean.isBuiltinAttribute n = do let m ← ST.Ref.get Lean.attributeMapRef pure (m.contains n)

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

Return the name of all registered attributes.

Equations

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

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

Equations

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

@[export lean_attribute_application_time]

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

Equations

• Lean.getBuiltinAttributeApplicationTime n = do let attr ← Lean.getBuiltinAttributeImpl n pure attr.applicationTime

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

Equations

• Lean.isAttribute env attrName = (Lean.PersistentEnvExtension.getState Lean.attributeExtension env).map.contains attrName

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Lean.Attribute.add declName attrName stx kind = do let __do_lift ← Lean.getEnv let attr ← Lean.ofExcept (Lean.getAttributeImpl __do_lift attrName) attr.add declName stx kind

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

Equations

• Lean.Attribute.erase declName attrName = do let __do_lift ← Lean.getEnv let attr ← Lean.ofExcept (Lean.getAttributeImpl __do_lift attrName) attr.erase declName

@[export lean_update_env_attributes]

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

updateEnvAttributes implementation

Equations

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

@[export lean_get_num_attributes]

def Lean.getNumBuiltinAttributesImpl : IO Nat

getNumBuiltinAttributes implementation

Equations

• Lean.getNumBuiltinAttributesImpl = do let __do_lift ← ST.Ref.get Lean.attributeMapRef pure __do_lift.size