Lean4
/-- 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](https://stacks.math.columbia.edu/tags) in the Stacks project or
[Tags page](https://kerodon.net/tag/) in the Kerodon project for more details.
-/
@[attr_parser 1000]
public meta def stacksTag : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.StacksTag.stacksTag 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.cat✝ `stacksTagDB 0)
(ParserDescr.parser✝ `Mathlib.StacksTag.stacksTagParser))
(ParserDescr.unary✝ `optional
(ParserDescr.binary✝ `andthen (ParserDescr.const✝ `ppSpace) (ParserDescr.const✝ `str))))
