inductive Lean.AttributeApplicationTime : Type

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

Instances For

• Lean.instBEqAttributeApplicationTime
• Lean.instInhabitedAttributeApplicationTime

instance Lean.instInhabitedAttributeApplicationTime : Inhabited AttributeApplicationTime

Equations

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

instance Lean.instBEqAttributeApplicationTime : BEq AttributeApplicationTime

Equations

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

@[reducible, inline]

abbrev Lean.AttrM (α : Type) : Type

Equations

• Lean.AttrM = Lean.CoreM

Instances For

• Lean.instMonadLiftImportMAttrM

instance Lean.instMonadLiftImportMAttrM : MonadLift ImportM AttrM

Equations

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

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

Instances For

• Lean.instInhabitedAttributeImplCore

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

Instances For

• Lean.instBEqAttributeKind
• Lean.instInhabitedAttributeKind
• Lean.instToStringAttributeKind

instance Lean.instBEqAttributeKind : BEq AttributeKind

Equations

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

instance Lean.instInhabitedAttributeKind : Inhabited AttributeKind

Equations

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

instance Lean.instToStringAttributeKind : ToString AttributeKind

Equations

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

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

Instances For

• Lean.instInhabitedAttributeImpl

instance Lean.instInhabitedAttributeImpl : Inhabited AttributeImpl

Equations

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

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

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

Equations

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

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

Equations

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

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

Equations

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

def Lean.Attribute.Builtin.getId? (stx : Syntax) : AttrM (Option 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 : Syntax) : AttrM Name

Equations

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

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

Equations

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

def Lean.Attribute.Builtin.getPrio (stx : Syntax) : 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 : AttributeImpl
• ext : PersistentEnvExtension Name Name NameSet

Instances For

• Lean.instInhabitedTagAttribute

instance Lean.instInhabitedTagAttribute : Inhabited TagAttribute

Equations

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

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

Equations

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

def Lean.TagAttribute.hasTag (attr : TagAttribute) (env : Environment) (decl : 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 : AttributeImpl
• ext : PersistentEnvExtension (Name × α) (Name × α) (NameMap α)

Instances For

• Lean.instInhabitedParametricAttribute

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

Equations

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

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 α)

Equations

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

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

Equations

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

def Lean.ParametricAttribute.setParam {α : Type} (attr : ParametricAttribute α) (env : Environment) (decl : Name) (param : α) : Except String 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 AttributeImpl
• ext : PersistentEnvExtension (Name × α) (Name × α) (NameMap α)

Instances For

• Lean.instInhabitedEnumAttributes

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

Equations

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

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 α)

Equations

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

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

Equations

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

def Lean.EnumAttributes.setValue {α : Type} (attrs : EnumAttributes α) (env : Environment) (decl : Name) (val : α) : Except String 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 = (Lean.Name → List Lean.DataValue → Except String Lean.AttributeImpl)

@[reducible, inline]

abbrev Lean.AttributeImplBuilderTable : Type

Equations

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

opaque Lean.attributeImplBuilderTableRef : IO.Ref AttributeImplBuilderTable

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

Equations

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

structure Lean.AttributeExtensionOLeanEntry : Type

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

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

Equations

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

structure Lean.AttributeExtensionState : Type

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

Instances For

• Lean.instInhabitedAttributeExtensionState

instance Lean.instInhabitedAttributeExtensionState : Inhabited 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 : Environment) (opts : Options) (declName : Name) : Except String AttributeImpl

Equations

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

@[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.

Equations

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

def Lean.getBuiltinAttributeNames : IO (List 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 : Name) : IO AttributeImpl

Equations

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

@[export lean_attribute_application_time]

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def Lean.Attribute.add (declName attrName : Name) (stx : Syntax) (kind : AttributeKind := AttributeKind.global) : 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 attrName : Name) : 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 : Environment) : IO 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