- afterTypeChecking: Lean.AttributeApplicationTime
- afterCompilation: Lean.AttributeApplicationTime
- beforeElaboration: Lean.AttributeApplicationTime
Instances For
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
- 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
Instances For
Equations
- Lean.instInhabitedAttributeImplCore = { default := Lean.AttributeImplCore.mk default default default }
- 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.
Instances For
Equations
- Lean.instBEqAttributeKind = { beq := Lean.beqAttributeKind✝ }
Equations
- Lean.instInhabitedAttributeKind = { default := Lean.AttributeKind.global }
Equations
- One or more equations did not get rendered due to their size.
- 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
Instances For
Equations
- Lean.instInhabitedAttributeImpl = { default := { toAttributeImplCore := default, add := default, erase := default } }
Low level attribute registration function.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.Attribute.Builtin.getId? stx = do let ident? ← Lean.Attribute.Builtin.getIdent? stx pure (Lean.Syntax.getId <$> ident?)
Instances For
Equations
- Lean.Attribute.Builtin.getId stx = do let __do_lift ← Lean.Attribute.Builtin.getIdent stx pure (Lean.Syntax.getId __do_lift)
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
- attr : Lean.AttributeImpl
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
.
Instances For
Equations
- Lean.instInhabitedTagAttribute = { default := { attr := default, ext := default } }
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
- 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
.
Instances For
Equations
- Lean.instInhabitedParametricAttribute = { default := { attr := default, ext := default } }
- 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
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
- 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.
Instances For
Equations
- Lean.instInhabitedEnumAttributes = { default := { attrs := default, ext := default } }
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Attribute extension and builders. We use builders to implement attribute factories for parser categories.
Equations
Instances For
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
- decl: Lake.Name → Lean.AttributeExtensionOLeanEntry
- builder: Lake.Name → Lake.Name → List Lean.DataValue → Lean.AttributeExtensionOLeanEntry
Instances For
- newEntries : List Lean.AttributeExtensionOLeanEntry
Instances For
Equations
- Lean.instInhabitedAttributeExtensionState = { default := { newEntries := default, map := default } }
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
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)
Instances For
Return the name of all registered attributes.
Equations
- Lean.getBuiltinAttributeNames = do let __do_lift ← ST.Ref.get Lean.attributeMapRef pure (Lean.PersistentHashMap.foldl __do_lift (fun r n x => n :: r) [])
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.getBuiltinAttributeApplicationTime n = do let attr ← Lean.getBuiltinAttributeImpl n pure attr.toAttributeImplCore.applicationTime
Instances For
Equations
- Lean.isAttribute env attrName = Lean.PersistentHashMap.contains (Lean.PersistentEnvExtension.getState Lean.attributeExtension env).map attrName
Instances For
Equations
- Lean.getAttributeNames env = let m := (Lean.PersistentEnvExtension.getState Lean.attributeExtension env).map; Lean.PersistentHashMap.foldl m (fun r n x => n :: r) []
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.Attribute.add declName attrName stx kind = do let __do_lift ← Lean.getEnv let attr ← Lean.ofExcept (Lean.getAttributeImpl __do_lift attrName) Lean.AttributeImpl.add attr declName stx kind
Instances For
Equations
- Lean.Attribute.erase declName attrName = do let __do_lift ← Lean.getEnv let attr ← Lean.ofExcept (Lean.getAttributeImpl __do_lift attrName) Lean.AttributeImpl.erase attr declName
Instances For
updateEnvAttributes
implementation
Equations
- One or more equations did not get rendered due to their size.
Instances For
getNumBuiltinAttributes
implementation
Equations
- Lean.getNumBuiltinAttributesImpl = do let __do_lift ← ST.Ref.get Lean.attributeMapRef pure __do_lift.size