Documentation

Mathlib.Tactic.StacksAttribute

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

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.

  • The online database where the tag is found.

  • tag : String

    The database tag.

  • comment : String

    The (optional) comment that comes with the given tag.

def Mathlib.StacksTag.addTagEntry {m : TypeType} [Lean.MonadEnv m] (declName : Lean.Name) (db : Mathlib.StacksTag.Database) (tag : String) (comment : String) :

addTagEntry declName tag comment takes as input the Name declName of a declaration and the Strings 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.
@[reducible, inline]

stacksTag is the node kind of Stacks Project Tags: a sequence of digits and uppercase letters.

Equations

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

Extract the underlying tag as a string from a stacksTag node.

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

The syntax for a "stacks" database identifier in a @[stacks] attribute.

Equations

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.