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
• @[dlmf REF] — DLMF

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

• dlmf : Database
• 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)

@[instance_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.dlmf = 0
• Mathlib.CrossRef.instHashableDatabase.hash Mathlib.CrossRef.Database.kerodon = 1
• Mathlib.CrossRef.instHashableDatabase.hash Mathlib.CrossRef.Database.lmfdb = 2
• Mathlib.CrossRef.instHashableDatabase.hash Mathlib.CrossRef.Database.stacks = 3
• Mathlib.CrossRef.instHashableDatabase.hash Mathlib.CrossRef.Database.wikidata = 4

@[instance_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

@[instance_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.dlmf.url = "https://dlmf.nist.gov/"
• 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.dlmf.label = "DLMF"
• 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.dlmf.shortName = "dlmf"
• 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

@[instance_reducible]

instance Mathlib.CrossRef.instBEqTag : BEq Tag

Equations

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

@[instance_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

DLMF parser

@[reducible, inline]

abbrev Mathlib.CrossRef.dlmfIdKind : Lean.SyntaxNodeKind

dlmfId is the node kind of DLMF references: generally <chapter_no>.<section_no>.E<equation_no> (e.g. 5.4.E1). See https://dlmf.nist.gov/help/cite for more details on the permalink format. Note that while underscores are not mentioned in the DLMF permalink table, they are supported and present in some actual links for equations.

Equations

• Mathlib.CrossRef.dlmfIdKind = `dlmfId

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

The main parser for DLMF references: generally <chapter_no>.<section_no>.E<equation_no> (e.g. 5.4.E1). See https://dlmf.nist.gov/help/cite for more details on the permalink format. Note that while underscores are not mentioned in the DLMF permalink table, they are supported and present in some actual links for equations.

Equations

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

def Mathlib.CrossRef.dlmfIdNoAntiquot : Lean.Parser.Parser

The main parser for DLMF references: generally <chapter_no>.<section_no>.E<equation_no> (e.g. 5.4.E1). See https://dlmf.nist.gov/help/cite for more details on the permalink format. Note that while underscores are not mentioned in the DLMF permalink table, they are supported and present in some actual links for equations.

Equations

• Mathlib.CrossRef.dlmfIdNoAntiquot = { info := Lean.Parser.mkAtomicInfo "dlmfId", fn := Mathlib.CrossRef.dlmfIdFn }

def Mathlib.CrossRef.dlmfIdParser : Lean.Parser.Parser

The main parser for DLMF references: generally <chapter_no>.<section_no>.E<equation_no> (e.g. 5.4.E1). See https://dlmf.nist.gov/help/cite for more details on the permalink format. Note that while underscores are not mentioned in the DLMF permalink table, they are supported and present in some actual links for equations.

Equations

• Mathlib.CrossRef.dlmfIdParser = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "dlmfId" Mathlib.CrossRef.dlmfIdKind) Mathlib.CrossRef.dlmfIdNoAntiquot

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.TSyntax.getDlmfId (stx : TSyntax Mathlib.CrossRef.dlmfIdKind) : CoreM String

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

Equations

• stx.getDlmfId = match Lean.Syntax.isLit? Mathlib.CrossRef.dlmfIdKind stx.raw with | some val => pure val | x => Lean.throwError (Lean.toMessageData "Malformed DLMF ref.")

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.Formatter.dlmfIdNoAntiquot.formatter : Formatter

The formatter for DLMF identifier syntax.

Equations

• Lean.PrettyPrinter.Formatter.dlmfIdNoAntiquot.formatter = Lean.PrettyPrinter.Formatter.visitAtom Mathlib.CrossRef.dlmfIdKind

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

def Lean.PrettyPrinter.Parenthesizer.dlmfIdAntiquot.parenthesizer : Parenthesizer

The parenthesizer for DLMF identifier syntax.

Equations

• Lean.PrettyPrinter.Parenthesizer.dlmfIdAntiquot.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.

DLMF attribute

def Mathlib.CrossRef.dlmfTag : Lean.ParserDescr

The dlmf attribute. Use it as @[dlmf 5.4.E1 "Optional comment"] to associate a Mathlib declaration with the corresponding DLMF 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.

def Mathlib.CrossRef.dlmfTags : Lean.ParserDescr

The #dlmf_tags command retrieves all declarations that have the dlmf attribute.

For each found declaration, it prints a line

'declaration_name' corresponds to tag 'declaration_tag'.

The variant #dlmf_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.