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.

inductive Mathlib.StacksTag.Database : Type

Web database users of projects tags

• kerodon : Database
• stacks : Database

instance Mathlib.StacksTag.instBEqDatabase : BEq Database

Equations

• Mathlib.StacksTag.instBEqDatabase = { beq := Mathlib.StacksTag.instBEqDatabase.beq }

def Mathlib.StacksTag.instBEqDatabase.beq : Database → Database → Bool

Equations

• Mathlib.StacksTag.instBEqDatabase.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Mathlib.StacksTag.instHashableDatabase.hash : Database → UInt64

Equations

• Mathlib.StacksTag.instHashableDatabase.hash Mathlib.StacksTag.Database.kerodon = 0
• Mathlib.StacksTag.instHashableDatabase.hash Mathlib.StacksTag.Database.stacks = 1

instance Mathlib.StacksTag.instHashableDatabase : Hashable Database

Equations

• Mathlib.StacksTag.instHashableDatabase = { hash := Mathlib.StacksTag.instHashableDatabase.hash }

structure Mathlib.StacksTag.Tag : Type

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.

instance Mathlib.StacksTag.instBEqTag : BEq Tag

Equations

• Mathlib.StacksTag.instBEqTag = { beq := Mathlib.StacksTag.instBEqTag.beq }

def Mathlib.StacksTag.instBEqTag.beq : Tag → Tag → Bool

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.StacksTag.instBEqTag.beq x✝¹ x✝ = false

instance Mathlib.StacksTag.instHashableTag : Hashable Tag

Equations

• Mathlib.StacksTag.instHashableTag = { hash := Mathlib.StacksTag.instHashableTag.hash }

def Mathlib.StacksTag.instHashableTag.hash : Tag → UInt64

Equations

• Mathlib.StacksTag.instHashableTag.hash { declName := a, database := a_1, tag := a_2, comment := a_3 } = mixHash (mixHash (mixHash (mixHash 0 (hash a)) (hash a_1)) (hash a_2)) (hash a_3)

opaque Mathlib.StacksTag.tagExt : Lean.SimplePersistentEnvExtension Tag (Std.HashSet Tag)

Defines the tagExt extension for adding a HashSet of Tags to the environment.

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

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]

abbrev Mathlib.StacksTag.stacksTagKind : Lean.SyntaxNodeKind

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

Equations

• Mathlib.StacksTag.stacksTagKind = `stacksTag

def Mathlib.StacksTag.stacksTagFn : Lean.Parser.ParserFn

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.

def Mathlib.StacksTag.stacksTagNoAntiquot : Lean.Parser.Parser

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 }

def Mathlib.StacksTag.stacksTagParser : Lean.Parser.Parser

The main parser for Stacks Project Tags: it accepts any sequence of 4 digits or uppercase letters.

Equations

• Mathlib.StacksTag.stacksTagParser = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "stacksTag" Mathlib.StacksTag.stacksTagKind) Mathlib.StacksTag.stacksTagNoAntiquot

def Lean.TSyntax.getStacksTag (stx : TSyntax Mathlib.StacksTag.stacksTagKind) : CoreM String

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")

def Lean.PrettyPrinter.Formatter.stacksTagNoAntiquot.formatter : Formatter

The formatter for Stacks Project Tags syntax.

Equations

• Lean.PrettyPrinter.Formatter.stacksTagNoAntiquot.formatter = Lean.PrettyPrinter.Formatter.visitAtom Mathlib.StacksTag.stacksTagKind

def Lean.PrettyPrinter.Parenthesizer.stacksTagAntiquot.parenthesizer : Parenthesizer

The parenthesizer for Stacks Project Tags syntax.

Equations

• Lean.PrettyPrinter.Parenthesizer.stacksTagAntiquot.parenthesizer = Lean.PrettyPrinter.Parenthesizer.visitToken

def Lean.Parser.Category.stacksTagDB : Category

The syntax category for the database name.

Equations

• Lean.Parser.Category.stacksTagDB = { }

def Mathlib.StacksTag.stacksTagDB.quot : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.StacksTag.stacksTagDBKerodon : Lean.ParserDescr

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")

def Mathlib.StacksTag.stacksTagDBStacks : Lean.ParserDescr

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")

def Mathlib.StacksTag.stacksTag : Lean.ParserDescr

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.

def Mathlib.StacksTag.traceStacksTags (db : Database) (verbose : Bool := false) : Lean.Elab.Command.CommandElabM Unit

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.

def Mathlib.StacksTag.stacksTags : Lean.ParserDescr

#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.

def Mathlib.StacksTag.kerodonTags : Lean.ParserDescr

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.