The environment extension for the attribute.
- base : Lean.NameHashSet
A list of "base" declarations which have been pre-tagged.
TagAttributeExtra
works around a limitation of TagAttribute
, which is that definitions
must be tagged in the same file that declares the definition.
This works well for definitions in lean core, but for attributes declared outside the core
this is problematic because we may want to tag declarations created before the attribute
was defined.
To resolve this, we allow a one-time exception to the rule that attributes must be applied in the same file as the declaration: During the declaration of the attribute itself, we can tag arbitrary other definitions, but once the attribute is declared we must tag things in the same file as normal.
Instances For
Registers a new tag attribute. The extra
field is a list of definitions from other modules
which will be "pre-tagged" and are not subject to the usual restriction on tagging in the same
file as the declaration.
Note: The extra
fields bypass the validate
function -
we assume the builtins are also pre-validated.
Instances For
Does declaration decl
have the tag attr
?
Instances For
Get the list of declarations tagged with the tag attribute attr
.
Instances For
- attr : Lean.ParametricAttribute α
The underlying
ParametricAttribute
. - base : Lean.HashMap Lean.Name α
A list of pre-tagged declarations with their values.
ParametricAttributeExtra
works around a limitation of ParametricAttribute
, which is that
definitions must be tagged in the same file that declares the definition.
This works well for definitions in lean core, but for attributes declared outside the core
this is problematic because we may want to tag declarations created before the attribute
was defined.
To resolve this, we allow a one-time exception to the rule that attributes must be applied in the same file as the declaration: During the declaration of the attribute itself, we can tag arbitrary other definitions, but once the attribute is declared we must tag things in the same file as normal.
Instances For
Registers a new parametric attribute. The extra
field is a list of definitions from other modules
which will be "pre-tagged" and are not subject to the usual restriction on tagging in the same
file as the declaration.
Instances For
Gets the parameter of attribute attr
associated to declaration decl
,
or none
if decl
is not tagged.
Instances For
Applies attribute attr
to declaration decl
, given a value for the parameter.