The stacks
and kerodon
attributes #
This allows tagging of mathlib results with the corresponding tags from the Stacks Project and Kerodon.
While the Stacks Project is the main focus, because the tag format at Kerodon is compatible, the attribute can be used to tag results with Kerodon tags as well.
Web database users of projects tags
Instances For
Tag
is the structure that carries the data of a project tag and a corresponding
Mathlib declaration.
- declName : Lean.Name
The name of the declaration with the given tag.
- database : Database
The online database where the tag is found.
- tag : String
The database tag.
- comment : String
The (optional) comment that comes with the given tag.
Instances For
addTagEntry declName tag comment
takes as input the Name
declName
of a declaration and
the String
s tag
and comment
of the stacks
attribute.
It extends the Tag
environment extension with the data declName, tag, comment
.
Equations
Instances For
stacksTag
is the node kind of Stacks Project Tags: a sequence of digits and
uppercase letters.
Equations
Instances For
The main parser for Stacks Project Tags: it accepts any sequence of 4 digits or uppercase letters.
Equations
Instances For
The main parser for Stacks Project Tags: it accepts any sequence of 4 digits or uppercase letters.
Equations
Instances For
The main parser for Stacks Project Tags: it accepts any sequence of 4 digits or uppercase letters.
Equations
Instances For
The formatter for Stacks Project Tags syntax.
Equations
Instances For
The parenthesizer for Stacks Project Tags syntax.
Equations
Instances For
The syntax category for the database name.
Equations
Instances For
The syntax for a "kerodon" database identifier in a @[kerodon]
attribute.
Equations
Instances For
The syntax for a "stacks" database identifier in a @[stacks]
attribute.
Equations
Instances For
The stacksTag
attribute.
Use it as @[kerodon TAG "Optional comment"]
or @[stacks TAG "Optional comment"]
depending on the database you are referencing.
The TAG
is mandatory and should be a sequence of 4 digits or uppercase letters.
See the Tags page in the Stacks project or Tags page in the Kerodon project for more details.
Equations
Instances For
traceStacksTags db verbose
prints the tags of the database db
to the user and
inlines the theorem statements if verbose
is true
.