A builder for attributes that are applied to declarations of a common type and
group them by the given attribute argument (an arbitrary Name
, currently).
Also creates a second "builtin" attribute used for bootstrapping, which saves
the applied declarations in an IO.Ref
instead of an environment extension.
Used to register elaborators, macros, tactics, and delaborators.
KeyedDeclsAttribute
definition.
Important: mkConst valueTypeName
and γ
must be definitionally equal.
- builtinName : Name
Builtin attribute name, if any (e.g., `builtin_term_elab)
- name : Name
Attribute name (e.g., `term_elab)
- descr : String
Attribute description
- valueTypeName : Name
Convert
Syntax
into aKey
, the default implementation expects an identifier.
Instances For
- key : Key
- declName : Name
Name of a declaration stored in the environment which has type
mkConst Def.valueTypeName
.
Instances For
- value : γ
Recall that we cannot store
γ
into .olean files because it is a closure. GivenOLeanEntry.declName
, we convert it into aγ
by using the unsafe functionevalConstCheck
.
Instances For
Equations
Instances For
Equations
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Retrieve entries tagged with [attr key]
or [builtinAttr key]
.
Equations
Instances For
Retrieve values tagged with [attr key]
or [builtinAttr key]
.