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
- kerodon: Mathlib.StacksTag.Database
- stacks: Mathlib.StacksTag.Database
Equations
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 : Mathlib.StacksTag.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.
Equations
Equations
Defines the tagExt
extension for adding a HashSet
of Tag
s
to the environment.
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
- One or more equations did not get rendered due to their size.
stacksTag
is the node kind of Stacks Project Tags: a sequence of digits and
uppercase letters.
Equations
- Mathlib.StacksTag.stacksTagKind = `stacksTag
The main parser for Stacks Project Tags: it accepts any sequence of 4 digits or uppercase letters.
Equations
- One or more equations did not get rendered due to their size.
The main parser for Stacks Project Tags: it accepts any sequence of 4 digits or uppercase letters.
Equations
- Mathlib.StacksTag.stacksTagNoAntiquot = { info := Lean.Parser.mkAtomicInfo "stacksTag", fn := Mathlib.StacksTag.stacksTagFn }
The main parser for Stacks Project Tags: it accepts any sequence of 4 digits or uppercase letters.
Extract the underlying tag as a string from a stacksTag
node.
Equations
- stx.getStacksTag = match Lean.Syntax.isLit? Mathlib.StacksTag.stacksTagKind stx.raw with | some val => pure val | x => Lean.throwError (Lean.toMessageData "Malformed Stacks tag")
The formatter for Stacks Project Tags syntax.
The parenthesizer for Stacks Project Tags syntax.
The syntax category for the database name.
Equations
Equations
- One or more equations did not get rendered due to their size.
The syntax for a "kerodon" database identifier in a @[kerodon]
attribute.
Equations
- Mathlib.StacksTag.stacksTagDBKerodon = Lean.ParserDescr.node `Mathlib.StacksTag.stacksTagDBKerodon 1024 (Lean.ParserDescr.symbol "kerodon")
The syntax for a "stacks" database identifier in a @[stacks]
attribute.
Equations
- Mathlib.StacksTag.stacksTagDBStacks = Lean.ParserDescr.node `Mathlib.StacksTag.stacksTagDBStacks 1024 (Lean.ParserDescr.symbol "stacks")
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
- One or more equations did not get rendered due to their size.
traceStacksTags db verbose
prints the tags of the database db
to the user and
inlines the theorem statements if verbose
is true
.
Equations
- One or more equations did not get rendered due to their size.
#stacks_tags
retrieves all declarations that have the stacks
attribute.
For each found declaration, it prints a line
'declaration_name' corresponds to tag 'declaration_tag'.
The variant #stacks_tags!
also adds the theorem statement after each summary line.
Equations
- One or more equations did not get rendered due to their size.
The #kerodon_tags
command retrieves all declarations that have the kerodon
attribute.
For each found declaration, it prints a line
'declaration_name' corresponds to tag 'declaration_tag'.
The variant #kerodon_tags!
also adds the theorem statement after each summary line.
Equations
- One or more equations did not get rendered due to their size.