Cross-reference attributes

This file provides attributes for tagging Mathlib results with cross-references to entries in external mathematical databases:

• @[stacks TAG] — Stacks Project
• @[kerodon TAG] — Kerodon
• @[wikidata QID] — Wikidata
• @[lmfdb ID] — LMFDB

Each attribute records the cross-reference in an environment extension and appends a link to the declaration's docstring.

The shared infrastructure (Database, Tag, tagExt, addCrossRefDoc, traceCrossRefs) is database-agnostic; per-database code defines a parser, the attribute syntax, and the trace command.

inductive Mathlib.CrossRef.Database : Type

The supported external databases

• kerodon : Database
• lmfdb : Database
• stacks : Database
• wikidata : Database

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

Equations

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

@[implicit_reducible]

instance Mathlib.CrossRef.instBEqDatabase : BEq Database

Equations

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

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

Equations

• Mathlib.CrossRef.instHashableDatabase.hash Mathlib.CrossRef.Database.kerodon = 0
• Mathlib.CrossRef.instHashableDatabase.hash Mathlib.CrossRef.Database.lmfdb = 1
• Mathlib.CrossRef.instHashableDatabase.hash Mathlib.CrossRef.Database.stacks = 2
• Mathlib.CrossRef.instHashableDatabase.hash Mathlib.CrossRef.Database.wikidata = 3

@[implicit_reducible]

instance Mathlib.CrossRef.instHashableDatabase : Hashable Database

Equations

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

def Mathlib.CrossRef.instOrdDatabase.ord : Database → Database → Ordering

Equations

• Mathlib.CrossRef.instOrdDatabase.ord x✝ y✝ = compare x✝.ctorIdx y✝.ctorIdx

@[implicit_reducible]

instance Mathlib.CrossRef.instOrdDatabase : Ord Database

Equations

• Mathlib.CrossRef.instOrdDatabase = { compare := Mathlib.CrossRef.instOrdDatabase.ord }

def Mathlib.CrossRef.Database.url : Database → String

The base URL for an external database's tag pages. Always ends with /.

Equations

• Mathlib.CrossRef.Database.kerodon.url = "https://kerodon.net/tag/"
• Mathlib.CrossRef.Database.lmfdb.url = "https://www.lmfdb.org/knowledge/show/"
• Mathlib.CrossRef.Database.stacks.url = "https://stacks.math.columbia.edu/tag/"
• Mathlib.CrossRef.Database.wikidata.url = "https://www.wikidata.org/wiki/"

def Mathlib.CrossRef.Database.label : Database → String

The display label used in docstring links and trace output.

Equations

• Mathlib.CrossRef.Database.kerodon.label = "Kerodon Tag"
• Mathlib.CrossRef.Database.lmfdb.label = "LMFDB"
• Mathlib.CrossRef.Database.stacks.label = "Stacks Tag"
• Mathlib.CrossRef.Database.wikidata.label = "Wikidata"

def Mathlib.CrossRef.Database.shortName : Database → String

A lowercase short name for the given database. Useful when exporting to JSON.

Equations

• Mathlib.CrossRef.Database.kerodon.shortName = "kerodon"
• Mathlib.CrossRef.Database.lmfdb.shortName = "lmfdb"
• Mathlib.CrossRef.Database.stacks.shortName = "stacks"
• Mathlib.CrossRef.Database.wikidata.shortName = "wikidata"

structure Mathlib.CrossRef.Tag : Type

A cross-reference from a Mathlib declaration to an entry in an external database.

• declName : Lean.Name

  The name of the declaration carrying the cross-reference.

• database : Database

  The external database the entry belongs to.

• tag : String

  The database identifier.

• comment : String

  An optional comment supplied with the attribute.

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

Equations

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

@[implicit_reducible]

instance Mathlib.CrossRef.instBEqTag : BEq Tag

Equations

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

@[implicit_reducible]

instance Mathlib.CrossRef.instHashableTag : Hashable Tag

Equations

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

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

Equations

• Mathlib.CrossRef.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.CrossRef.tagExt : Lean.SimplePersistentEnvExtension Tag (Array (Array Tag))

The environment extension storing all cross-references. addImportedFn is a constant function to avoid a performance overhead during initialization.

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

addTagEntry declName db tag comment records a cross-reference for declName in tagExt.

Equations

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

def Mathlib.CrossRef.addCrossRefDoc (db : Database) (decl : Lean.Name) (idStr comment : String) : Lean.CoreM Unit

Append a cross-reference link to the docstring of decl and record it in tagExt. This is the database-agnostic core of every cross-reference attribute's add handler.

Equations

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

Stacks (and Kerodon) parser

@[reducible, inline]

abbrev Mathlib.CrossRef.stacksTagKind : Lean.SyntaxNodeKind

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

Equations

• Mathlib.CrossRef.stacksTagKind = `stacksTag

def Mathlib.CrossRef.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.CrossRef.stacksTagNoAntiquot : Lean.Parser.Parser

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

Equations

• Mathlib.CrossRef.stacksTagNoAntiquot = { info := Lean.Parser.mkAtomicInfo "stacksTag", fn := Mathlib.CrossRef.stacksTagFn }

def Mathlib.CrossRef.stacksTagParser : Lean.Parser.Parser

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

Equations

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

Wikidata parser

@[reducible, inline]

abbrev Mathlib.CrossRef.wikidataIdKind : Lean.SyntaxNodeKind

wikidataId is the node kind of Wikidata identifiers: the letter Q followed by digits.

Equations

• Mathlib.CrossRef.wikidataIdKind = `wikidataId

def Mathlib.CrossRef.wikidataIdFn : Lean.Parser.ParserFn

The main parser for Wikidata identifiers: it accepts Q followed by one or more digits.

Equations

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

def Mathlib.CrossRef.wikidataIdNoAntiquot : Lean.Parser.Parser

The main parser for Wikidata identifiers: it accepts Q followed by one or more digits.

Equations

• Mathlib.CrossRef.wikidataIdNoAntiquot = { info := Lean.Parser.mkAtomicInfo "wikidataId", fn := Mathlib.CrossRef.wikidataIdFn }

def Mathlib.CrossRef.wikidataIdParser : Lean.Parser.Parser

The main parser for Wikidata identifiers: it accepts Q followed by one or more digits.

Equations

• Mathlib.CrossRef.wikidataIdParser = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "wikidataId" Mathlib.CrossRef.wikidataIdKind) Mathlib.CrossRef.wikidataIdNoAntiquot

LMFDB parser

@[reducible, inline]

abbrev Mathlib.CrossRef.lmfdbIdKind : Lean.SyntaxNodeKind

lmfdbId is the node kind of LMFDB identifiers: lower case words with . in between. The words can also contain underscores and digits.

Equations

• Mathlib.CrossRef.lmfdbIdKind = `lmfdbId

def Mathlib.CrossRef.lmfdbIdFn : Lean.Parser.ParserFn

The main parser for LMFDB identifiers: it accepts lower case words with . in between. The words can also contain underscores and digits.

Equations

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

def Mathlib.CrossRef.lmfdbIdNoAntiquot : Lean.Parser.Parser

The main parser for LMFDB identifiers: it accepts lower case words with . in between. The words can also contain underscores and digits.

Equations

• Mathlib.CrossRef.lmfdbIdNoAntiquot = { info := Lean.Parser.mkAtomicInfo "lmfdbId", fn := Mathlib.CrossRef.lmfdbIdFn }

def Mathlib.CrossRef.lmfdbIdParser : Lean.Parser.Parser

The main parser for LMFDB identifiers: it accepts lower case words with . in between. The words can also contain underscores and digits.

Equations

• Mathlib.CrossRef.lmfdbIdParser = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "lmfdbId" Mathlib.CrossRef.lmfdbIdKind) Mathlib.CrossRef.lmfdbIdNoAntiquot

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

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

Equations

• stx.getStacksTag = match Lean.Syntax.isLit? Mathlib.CrossRef.stacksTagKind stx.raw with | some val => pure val | x => Lean.throwError (Lean.toMessageData "Malformed Stacks tag")

def Lean.TSyntax.getWikidataId (stx : TSyntax Mathlib.CrossRef.wikidataIdKind) : CoreM String

Extract the underlying identifier as a string from a wikidataId node.

Equations

• stx.getWikidataId = match Lean.Syntax.isLit? Mathlib.CrossRef.wikidataIdKind stx.raw with | some val => pure val | x => Lean.throwError (Lean.toMessageData "Malformed Wikidata id")

def Lean.TSyntax.getLmfdbId (stx : TSyntax Mathlib.CrossRef.lmfdbIdKind) : CoreM String

Extract the underlying identifier as a string from a lmfdbId node.

Equations

• stx.getLmfdbId = match Lean.Syntax.isLit? Mathlib.CrossRef.lmfdbIdKind stx.raw with | some val => pure val | x => Lean.throwError (Lean.toMessageData "Malformed LMFDB id")

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.CrossRef.stacksTagKind

def Lean.PrettyPrinter.Formatter.wikidataIdNoAntiquot.formatter : Formatter

The formatter for Wikidata identifier syntax.

Equations

• Lean.PrettyPrinter.Formatter.wikidataIdNoAntiquot.formatter = Lean.PrettyPrinter.Formatter.visitAtom Mathlib.CrossRef.wikidataIdKind

def Lean.PrettyPrinter.Formatter.lmfdbIdNoAntiquot.formatter : Formatter

The formatter for LMFDB identifier syntax.

Equations

• Lean.PrettyPrinter.Formatter.lmfdbIdNoAntiquot.formatter = Lean.PrettyPrinter.Formatter.visitAtom Mathlib.CrossRef.lmfdbIdKind

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.PrettyPrinter.Parenthesizer.wikidataIdAntiquot.parenthesizer : Parenthesizer

The parenthesizer for Wikidata identifier syntax.

Equations

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

def Lean.PrettyPrinter.Parenthesizer.lmfdbIdAntiquot.parenthesizer : Parenthesizer

The parenthesizer for LMFDB identifier syntax.

Equations

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

Stacks / Kerodon attribute

def Lean.Parser.Category.stacksTagDB : Category

The syntax category for the database name.

Equations

• Lean.Parser.Category.stacksTagDB = { }

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

Equations

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

def Mathlib.CrossRef.stacksTagDBKerodon : Lean.ParserDescr

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

Equations

• Mathlib.CrossRef.stacksTagDBKerodon = Lean.ParserDescr.node `Mathlib.CrossRef.stacksTagDBKerodon 1024 (Lean.ParserDescr.symbol "kerodon")

def Mathlib.CrossRef.stacksTagDBStacks : Lean.ParserDescr

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

Equations

• Mathlib.CrossRef.stacksTagDBStacks = Lean.ParserDescr.node `Mathlib.CrossRef.stacksTagDBStacks 1024 (Lean.ParserDescr.symbol "stacks")

def Mathlib.CrossRef.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.

Wikidata attribute

def Mathlib.CrossRef.wikidataTag : Lean.ParserDescr

The wikidata attribute. Use it as @[wikidata Q12345 "Optional comment"] to associate a Mathlib declaration with the corresponding Wikidata item.

The identifier must be the letter Q followed by one or more digits.

Equations

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

LMFDB attribute

def Mathlib.CrossRef.lmfdbTag : Lean.ParserDescr

The lmfdb attribute. Use it as @[lmfdb foo.bar "Optional comment"] to associate a Mathlib declaration with the corresponding LMFDB item.

Equations

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

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

traceCrossRefs db verbose prints the cross-references of database db and inlines the declaration types if verbose is true.

Equations

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

def Mathlib.CrossRef.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 (for theorems) or declaration type (for definitions, structures, instances, etc.) after each summary line.

Equations

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

def Mathlib.CrossRef.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 (for theorems) or declaration type (for definitions, structures, instances, etc.) after each summary line.

Equations

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

def Mathlib.CrossRef.wikidataTags : Lean.ParserDescr

The #wikidata_tags command retrieves all declarations that have the wikidata attribute.

For each found declaration, it prints a line

'declaration_name' corresponds to tag 'declaration_tag'.

The variant #wikidata_tags! also adds the theorem statement (for theorems) or declaration type (for definitions, structures, instances, etc.) after each summary line.

Equations

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

def Mathlib.CrossRef.lmfdbTags : Lean.ParserDescr

The #lmfdb_tags command retrieves all declarations that have the lmfdb attribute.

For each found declaration, it prints a line

'declaration_name' corresponds to tag 'declaration_tag'.

The variant #lmfdb_tags! also adds the theorem statement (for theorems) or declaration type (for definitions, structures, instances, etc.) after each summary line.

Equations

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