The zz_tag attribute

@[zz_tag "TAG"] records which numbered result of the source paper a declaration formalizes, TAG being that result's label (def_f_z, lem_bessel_F, prop_simple_real_lower, thm_simple, ...). It is the analogue of Mathlib's @[stacks TAG].

The tag goes on every declaration whose union states the result's content, not merely the first; scaffolding — helper definitions, hypothesis bundles, proof-local lemmas — stays untagged.

def zzTag : Lean.ParserDescr

@[zz_tag "TAG"] records which result of the source paper a declaration formalizes.

The syntax node is named zzTag, not zz_tag: the user-facing token keeps the underscore, to match @[stacks …], but Mathlib's defsWithUnderscore linter inspects the declaration name, so the internal name must be lowerCamelCase.

Equations

• zzTag = Lean.ParserDescr.node `zzTag 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "zz_tag " false) (Lean.ParserDescr.const `str))

opaque zzTagAttr : Lean.ParametricAttribute String

Records which result of the source paper a declaration formalizes.