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@[pibase <topic> ID]— π-Base databases (by topic)@[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.
Equations
Equations
- Mathlib.CrossRef.instBEqPiBaseTopic.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)
Instances For
Equations
- Mathlib.CrossRef.instOrdPiBaseTopic.ord x✝ y✝ = compare x✝.ctorIdx y✝.ctorIdx
Instances For
Equations
The string such that https://{topic.urlSubdomain}.pi-base.org is the base URL of the π-Base
project identified by this topic.
Equations
- Mathlib.CrossRef.PiBaseTopic.topology.urlSubdomain = "topology"
Instances For
The display label used in docstring links and trace output. Used in Database.label.
Equations
- Mathlib.CrossRef.PiBaseTopic.topology.label = "Topology"
Instances For
A lowercase short name for the given database. Used in Database.shortName. Useful when
exporting to JSON.
Equations
- Mathlib.CrossRef.PiBaseTopic.topology.shortName = "topology"
Instances For
Equations
Equations
- Mathlib.CrossRef.instBEqDatabase.beq Mathlib.CrossRef.Database.dlmf Mathlib.CrossRef.Database.dlmf = true
- Mathlib.CrossRef.instBEqDatabase.beq Mathlib.CrossRef.Database.kerodon Mathlib.CrossRef.Database.kerodon = true
- Mathlib.CrossRef.instBEqDatabase.beq Mathlib.CrossRef.Database.lmfdb Mathlib.CrossRef.Database.lmfdb = true
- Mathlib.CrossRef.instBEqDatabase.beq (Mathlib.CrossRef.Database.pibase a) (Mathlib.CrossRef.Database.pibase b) = (a == b)
- Mathlib.CrossRef.instBEqDatabase.beq Mathlib.CrossRef.Database.stacks Mathlib.CrossRef.Database.stacks = true
- Mathlib.CrossRef.instBEqDatabase.beq Mathlib.CrossRef.Database.wikidata Mathlib.CrossRef.Database.wikidata = true
- Mathlib.CrossRef.instBEqDatabase.beq x✝¹ x✝ = false
Instances For
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.pibase a) = mixHash 3 (hash a)
- Mathlib.CrossRef.instHashableDatabase.hash Mathlib.CrossRef.Database.stacks = 4
- Mathlib.CrossRef.instHashableDatabase.hash Mathlib.CrossRef.Database.wikidata = 5
Instances For
Equations
Equations
- Mathlib.CrossRef.instOrdDatabase.ord Mathlib.CrossRef.Database.dlmf Mathlib.CrossRef.Database.dlmf = Ordering.eq
- Mathlib.CrossRef.instOrdDatabase.ord Mathlib.CrossRef.Database.dlmf x✝ = Ordering.lt
- Mathlib.CrossRef.instOrdDatabase.ord x✝ Mathlib.CrossRef.Database.dlmf = Ordering.gt
- Mathlib.CrossRef.instOrdDatabase.ord Mathlib.CrossRef.Database.kerodon Mathlib.CrossRef.Database.kerodon = Ordering.eq
- Mathlib.CrossRef.instOrdDatabase.ord Mathlib.CrossRef.Database.kerodon x✝ = Ordering.lt
- Mathlib.CrossRef.instOrdDatabase.ord x✝ Mathlib.CrossRef.Database.kerodon = Ordering.gt
- Mathlib.CrossRef.instOrdDatabase.ord Mathlib.CrossRef.Database.lmfdb Mathlib.CrossRef.Database.lmfdb = Ordering.eq
- Mathlib.CrossRef.instOrdDatabase.ord Mathlib.CrossRef.Database.lmfdb x✝ = Ordering.lt
- Mathlib.CrossRef.instOrdDatabase.ord x✝ Mathlib.CrossRef.Database.lmfdb = Ordering.gt
- Mathlib.CrossRef.instOrdDatabase.ord (Mathlib.CrossRef.Database.pibase a) (Mathlib.CrossRef.Database.pibase b) = (compare a b).then Ordering.eq
- Mathlib.CrossRef.instOrdDatabase.ord (Mathlib.CrossRef.Database.pibase a) x✝ = Ordering.lt
- Mathlib.CrossRef.instOrdDatabase.ord x✝ (Mathlib.CrossRef.Database.pibase a) = Ordering.gt
- Mathlib.CrossRef.instOrdDatabase.ord Mathlib.CrossRef.Database.stacks Mathlib.CrossRef.Database.stacks = Ordering.eq
- Mathlib.CrossRef.instOrdDatabase.ord Mathlib.CrossRef.Database.stacks x✝ = Ordering.lt
- Mathlib.CrossRef.instOrdDatabase.ord x✝ Mathlib.CrossRef.Database.stacks = Ordering.gt
- Mathlib.CrossRef.instOrdDatabase.ord Mathlib.CrossRef.Database.wikidata Mathlib.CrossRef.Database.wikidata = Ordering.eq
Instances For
Equations
The URL for an external database entry, where id is the identifier recorded in Tag.tag.
Equations
- One or more equations did not get rendered due to their size.
- Mathlib.CrossRef.Database.dlmf.url x✝ = toString "https://dlmf.nist.gov/" ++ toString x✝
- Mathlib.CrossRef.Database.kerodon.url x✝ = toString "https://kerodon.net/tag/" ++ toString x✝
- Mathlib.CrossRef.Database.lmfdb.url x✝ = toString "https://www.lmfdb.org/knowledge/show/" ++ toString x✝
- Mathlib.CrossRef.Database.stacks.url x✝ = toString "https://stacks.math.columbia.edu/tag/" ++ toString x✝
- Mathlib.CrossRef.Database.wikidata.url x✝ = toString "https://www.wikidata.org/wiki/" ++ toString x✝
Instances For
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.pibase a).label = toString "π-Base (" ++ toString a.label ++ toString ")"
- Mathlib.CrossRef.Database.stacks.label = "Stacks Tag"
- Mathlib.CrossRef.Database.wikidata.label = "Wikidata"
Instances For
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.pibase a).shortName = toString "pibase-" ++ toString a.shortName
- Mathlib.CrossRef.Database.stacks.shortName = "stacks"
- Mathlib.CrossRef.Database.wikidata.shortName = "wikidata"
Instances For
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.
Instances For
Equations
- One or more equations did not get rendered due to their size.
- Mathlib.CrossRef.instBEqTag.beq x✝¹ x✝ = false
Instances For
Equations
Equations
The environment extension storing all cross-references.
addImportedFn is a constant function to avoid a performance overhead during initialization.
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.
Instances For
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.
Instances For
Stacks (and Kerodon) parser #
stacksTag is the node kind of Stacks Project Tags: a sequence of digits and
uppercase letters.
Equations
- Mathlib.CrossRef.stacksTagKind = `stacksTag
Instances For
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.
Instances For
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 }
Instances For
The main parser for Stacks Project Tags: it accepts any sequence of 4 digits or uppercase letters.
Equations
Instances For
Wikidata parser #
wikidataId is the node kind of Wikidata identifiers: the letter Q followed by digits.
Equations
- Mathlib.CrossRef.wikidataIdKind = `wikidataId
Instances For
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.
Instances For
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 }
Instances For
The main parser for Wikidata identifiers: it accepts Q followed by one or more digits.
Equations
Instances For
LMFDB parser #
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
Instances For
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.
Instances For
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 }
Instances For
The main parser for LMFDB identifiers: it accepts lower case words with . in between.
The words can also contain underscores and digits.
Equations
Instances For
π-Base parser #
pibaseId is the node kind of π-Base identifiers: one of the letters P, S, or T,
followed by exactly six digits.
Equations
- Mathlib.CrossRef.pibaseIdKind = `pibaseId
Instances For
The main parser for π-Base identifiers: it accepts canonical property, space, and theorem
identifiers, such as P000001, S000023, and T000010.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The main parser for π-Base identifiers: it accepts canonical property, space, and theorem
identifiers, such as P000001, S000023, and T000010.
Equations
- Mathlib.CrossRef.pibaseIdNoAntiquot = { info := Lean.Parser.mkAtomicInfo "pibaseId", fn := Mathlib.CrossRef.pibaseIdFn }
Instances For
The main parser for π-Base identifiers: it accepts canonical property, space, and theorem
identifiers, such as P000001, S000023, and T000010.
Equations
Instances For
DLMF parser #
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
Instances For
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.
Instances For
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 }
Instances For
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
Instances For
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")
Instances For
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")
Instances For
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")
Instances For
Extract the underlying identifier as a string from a pibaseId node.
Equations
- stx.getPibaseId = match Lean.Syntax.isLit? Mathlib.CrossRef.pibaseIdKind stx.raw with | some val => pure val | x => Lean.throwError (Lean.toMessageData "Malformed π-Base id")
Instances For
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.")
Instances For
The formatter for Stacks Project Tags syntax.
Equations
Instances For
The formatter for Wikidata identifier syntax.
Equations
Instances For
The formatter for LMFDB identifier syntax.
Equations
Instances For
The formatter for π-Base identifier syntax.
Equations
Instances For
The formatter for DLMF identifier syntax.
Equations
Instances For
The parenthesizer for Stacks Project Tags syntax.
Equations
Instances For
The parenthesizer for Wikidata identifier syntax.
Equations
Instances For
The parenthesizer for LMFDB identifier syntax.
Equations
Instances For
The parenthesizer for π-Base identifier syntax.
Equations
Instances For
The parenthesizer for DLMF identifier syntax.
Equations
Instances For
Stacks / Kerodon attribute #
The syntax category for the database name.
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
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")
Instances For
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")
Instances For
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.
Instances For
Wikidata attribute #
LMFDB attribute #
π-Base attribute #
The topic identifying a π-Base database. Possible values:
This list will be expanded in the future.
Equations
- Mathlib.CrossRef.pibaseTopic = Lean.ParserDescr.nodeWithAntiquot "pibaseTopic" `Mathlib.CrossRef.pibaseTopic (Lean.ParserDescr.nonReservedSymbol "topology" false)
Instances For
Get the PiBaseTopic from a syntax key.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The pibase attribute.
Use it as @[pibase <topic> P000001 "Optional comment"] to associate a Mathlib declaration with
the corresponding π-Base property, space, or theorem.
Each <topic> identifies a different π-Base database. The possible values of <topic> are:
This list will be expanded in the future.
The identifier must start with P, S, or T, followed by exactly six digits.
Equations
- One or more equations did not get rendered due to their size.
Instances For
DLMF attribute #
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.
Instances For
#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.
Instances For
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.
Instances For
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.
Instances For
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.
Instances For
The #pibase_tags topic command retrieves all declarations that have the pibase attribute
with the given topic.
For each found declaration, it prints a line
'declaration_name' corresponds to tag 'declaration_tag'.
The variant #pibase_tags! topic 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.
Instances For
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.