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✝ }

@[inline]

abbrev Lean.AttrM (α : Type) : Type

Equations

• Lean.AttrM = Lean.CoreM

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

Equations

• Lean.instMonadLiftImportMAttrM = { monadLift := fun {α} x => do let a ← Lean.getEnv let a_1 ← Lean.getOptions liftM (x { env := a, opts := a_1 }) }

structure Lean.AttributeImplCore : Type

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

  ref : autoParam Lean.Name _auto✝
• name : Lean.Name
• descr : String
• applicationTime : Lean.AttributeApplicationTime

instance Lean.instInhabitedAttributeImplCore : Inhabited Lean.AttributeImplCore

Equations

• Lean.instInhabitedAttributeImplCore = { default := Lean.AttributeImplCore.mk default default default }

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

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

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

  add : Lean.Name → Lean.Syntax → Lean.AttributeKind → Lean.AttrM Unit
• erase : Lean.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 (Lean.PersistentHashMap Lean.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:

@[builtinAttrParser] def simple     := leading_parser ident >> optional ident >> optional priorityParser
/- We can't use `simple` for `class`, `instance`, `export` and `macro` because they are  keywords. -/
@[builtinAttrParser] def «class»    := leading_parser "class"
@[builtinAttrParser] def «instance» := leading_parser "instance" >> optional priorityParser
@[builtinAttrParser] 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

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 Lean.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 Lean.Name

Equations

• Lean.Attribute.Builtin.getId stx = do let a ← Lean.Attribute.Builtin.getIdent stx pure (Lean.Syntax.getId a)

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

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

Equations

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

def Lean.registerTagAttribute (name : Lean.Name) (descr : String) (validate : optParam (Lean.Name → Lean.AttrM Unit) fun x => pure ()) (ref : autoParam Lean.Name _auto✝) : 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 : Lean.Name) : Bool

Equations

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

structure Lean.ParametricAttribute (α : Type) : Type

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

Equations

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

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

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

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

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

Equations

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

def Lean.ParametricAttribute.getParam? {α : Type} [inst : Inhabited α] (attr : Lean.ParametricAttribute α) (env : Lean.Environment) (decl : Lean.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 : Lean.Name) (param : α) : Except String Lean.Environment

Equations

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

structure Lean.EnumAttributes (α : Type) : Type

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

Equations

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

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

Equations

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

def Lean.EnumAttributes.getValue {α : Type} [inst : Inhabited α] (attr : Lean.EnumAttributes α) (env : Lean.Environment) (decl : Lean.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 : Lean.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.

@[inline]

abbrev Lean.AttributeImplBuilder : Type

Equations

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

@[inline]

abbrev Lean.AttributeImplBuilderTable : Type

Equations

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

opaque Lean.attributeImplBuilderTableRef : IO.Ref Lean.AttributeImplBuilderTable

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

Equations

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

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

Equations

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

inductive Lean.AttributeExtensionOLeanEntry : Type

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

structure Lean.AttributeExtensionState : Type

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

instance Lean.instInhabitedAttributeExtensionState : Inhabited Lean.AttributeExtensionState

Equations

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

@[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 : Lean.Name) : Except String Lean.AttributeImpl

Equations

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

@[implementedBy Lean.mkAttributeImplOfConstantUnsafe]

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

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

Equations

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

opaque Lean.attributeExtension : Lean.AttributeExtension

@[export lean_is_attribute]

def Lean.isBuiltinAttribute (n : Lean.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 (Lean.PersistentHashMap.contains m n)

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

Return the name of all registered attributes.

Equations

• Lean.getBuiltinAttributeNames = do let a ← ST.Ref.get Lean.attributeMapRef pure (Lean.PersistentHashMap.foldl a (fun r n x => n :: r) [])

def Lean.getBuiltinAttributeImpl (attrName : Lean.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 : Lean.Name) : IO Lean.AttributeApplicationTime

Equations

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

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

Equations

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

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

Equations

• Lean.getAttributeNames env = let m := (Lean.PersistentEnvExtension.getState Lean.attributeExtension env).map; Lean.PersistentHashMap.foldl m (fun r n x => n :: r) []

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

Equations

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

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

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 : List Lean.DataValue) : IO Lean.Environment

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) (kind : optParam Lean.AttributeKind Lean.AttributeKind.global) : Lean.AttrM Unit

Equations

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

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

Equations

• Lean.Attribute.erase declName attrName = do let a ← Lean.getEnv let attr ← Lean.ofExcept (Lean.getAttributeImpl a attrName) Lean.AttributeImpl.erase attr 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.getNumBuiltiAttributesImpl : IO Nat

getNumBuiltinAttributes implementation

Equations

• Lean.getNumBuiltiAttributesImpl = do let a ← ST.Ref.get Lean.attributeMapRef pure a.size