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.

source

inductive Mathlib.CrossRef.PiBaseTopic :

Type

A topic identifying a π-Base project.

topology : PiBaseTopic

Instances For

source

@[instance_reducible]

instance Mathlib.CrossRef.instBEqPiBaseTopic :

BEq PiBaseTopic

source

def Mathlib.CrossRef.instBEqPiBaseTopic.beq :

PiBaseTopic → PiBaseTopic → Bool

Instances For

source

def Mathlib.CrossRef.instHashablePiBaseTopic.hash :

PiBaseTopic → UInt64

Instances For

source

@[instance_reducible]

instance Mathlib.CrossRef.instHashablePiBaseTopic :

Hashable PiBaseTopic

source

def Mathlib.CrossRef.instOrdPiBaseTopic.ord :

PiBaseTopic → PiBaseTopic → Ordering

Instances For

source

@[instance_reducible]

instance Mathlib.CrossRef.instOrdPiBaseTopic :

Ord PiBaseTopic

source

def Mathlib.CrossRef.PiBaseTopic.urlSubdomain :

PiBaseTopic → String

The string such that https://{topic.urlSubdomain}.pi-base.org is the base URL of the π-Base project identified by this topic.

Instances For

source

def Mathlib.CrossRef.PiBaseTopic.label :

PiBaseTopic → String

The display label used in docstring links and trace output. Used in Database.label.

Instances For

source

def Mathlib.CrossRef.PiBaseTopic.shortName :

PiBaseTopic → String

A lowercase short name for the given database. Used in Database.shortName. Useful when exporting to JSON.

Instances For

source

inductive Mathlib.CrossRef.Database :

Type

The supported external databases

dlmf : Database
kerodon : Database
lmfdb : Database
pibase (topic : PiBaseTopic) : Database
stacks : Database
wikidata : Database

Instances For

source

@[instance_reducible]

instance Mathlib.CrossRef.instBEqDatabase :

BEq Database

source

def Mathlib.CrossRef.instBEqDatabase.beq :

Database → Database → Bool

Instances For

source

def Mathlib.CrossRef.instHashableDatabase.hash :

Database → UInt64

Instances For

source

@[instance_reducible]

instance Mathlib.CrossRef.instHashableDatabase :

Hashable Database

source

def Mathlib.CrossRef.instOrdDatabase.ord :

Database → Database → Ordering

Instances For

source

@[instance_reducible]

instance Mathlib.CrossRef.instOrdDatabase :

Ord Database

source

def Mathlib.CrossRef.Database.url :

Database → String → String

The URL for an external database entry, where id is the identifier recorded in Tag.tag.

Instances For

source

def Mathlib.CrossRef.Database.label :

Database → String

The display label used in docstring links and trace output.

Instances For

source

def Mathlib.CrossRef.Database.shortName :

Database → String

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

Instances For

source

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.

Instances For

source

def Mathlib.CrossRef.instBEqTag.beq :

Tag → Tag → Bool

Instances For

source

@[instance_reducible]

instance Mathlib.CrossRef.instBEqTag :

BEq Tag

source

def Mathlib.CrossRef.instHashableTag.hash :

Tag → UInt64

Instances For

source

@[instance_reducible]

instance Mathlib.CrossRef.instHashableTag :

Hashable Tag

source

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.

source

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.

Instances For

source

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.

Instances For

Stacks (and Kerodon) parser #

source

@[reducible, inline]

abbrev Mathlib.CrossRef.stacksTagKind :

Lean.SyntaxNodeKind

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

Instances For

source

def Mathlib.CrossRef.stacksTagFn :

Lean.Parser.ParserFn

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

Instances For

source

def Mathlib.CrossRef.stacksTagNoAntiquot :

Lean.Parser.Parser

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

Instances For

source

def Mathlib.CrossRef.stacksTagParser :

Lean.Parser.Parser

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

Instances For

Wikidata parser #

source

@[reducible, inline]

abbrev Mathlib.CrossRef.wikidataIdKind :

Lean.SyntaxNodeKind

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

Instances For

source

def Mathlib.CrossRef.wikidataIdFn :

Lean.Parser.ParserFn

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

Instances For

source

def Mathlib.CrossRef.wikidataIdNoAntiquot :

Lean.Parser.Parser

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

Instances For

source

def Mathlib.CrossRef.wikidataIdParser :

Lean.Parser.Parser

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

Instances For

LMFDB parser #

source

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

Instances For

source

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.

Instances For

source

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.

Instances For

source

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.

Instances For

π-Base parser #

source

@[reducible, inline]

abbrev Mathlib.CrossRef.pibaseIdKind :

Lean.SyntaxNodeKind

pibaseId is the node kind of π-Base identifiers: one of the letters P, S, or T, followed by exactly six digits.

Instances For

source

def Mathlib.CrossRef.pibaseIdFn :

Lean.Parser.ParserFn

The main parser for π-Base identifiers: it accepts canonical property, space, and theorem identifiers, such as P000001, S000023, and T000010.

Instances For

source

def Mathlib.CrossRef.pibaseIdNoAntiquot :

Lean.Parser.Parser

The main parser for π-Base identifiers: it accepts canonical property, space, and theorem identifiers, such as P000001, S000023, and T000010.

Instances For

source

def Mathlib.CrossRef.pibaseIdParser :

Lean.Parser.Parser

The main parser for π-Base identifiers: it accepts canonical property, space, and theorem identifiers, such as P000001, S000023, and T000010.

Instances For

DLMF parser #

source

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

Instances For

source

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.

Instances For

source

def Mathlib.CrossRef.dlmfIdNoAntiquot :

Lean.Parser.Parser

Instances For

source

def Mathlib.CrossRef.dlmfIdParser :

Lean.Parser.Parser

Instances For

source

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

CoreM String

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

Instances For

source

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

CoreM String

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

Instances For

source

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

CoreM String

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

Instances For

source

def Lean.TSyntax.getPibaseId (stx : TSyntax Mathlib.CrossRef.pibaseIdKind) :

CoreM String

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

Instances For

source

def Lean.TSyntax.getDlmfId (stx : TSyntax Mathlib.CrossRef.dlmfIdKind) :

CoreM String

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

Instances For

source

def Lean.PrettyPrinter.Formatter.stacksTagNoAntiquot.formatter :

Formatter

The formatter for Stacks Project Tags syntax.

Instances For

source

def Lean.PrettyPrinter.Formatter.wikidataIdNoAntiquot.formatter :

Formatter

The formatter for Wikidata identifier syntax.

Instances For

source

def Lean.PrettyPrinter.Formatter.lmfdbIdNoAntiquot.formatter :

Formatter

The formatter for LMFDB identifier syntax.

Instances For

source

def Lean.PrettyPrinter.Formatter.pibaseIdNoAntiquot.formatter :

Formatter

The formatter for π-Base identifier syntax.

Instances For

source

def Lean.PrettyPrinter.Formatter.dlmfIdNoAntiquot.formatter :

Formatter

The formatter for DLMF identifier syntax.

Instances For

source

def Lean.PrettyPrinter.Parenthesizer.stacksTagAntiquot.parenthesizer :

Parenthesizer

The parenthesizer for Stacks Project Tags syntax.

Instances For

source

def Lean.PrettyPrinter.Parenthesizer.wikidataIdAntiquot.parenthesizer :

Parenthesizer

The parenthesizer for Wikidata identifier syntax.

Instances For

source

def Lean.PrettyPrinter.Parenthesizer.lmfdbIdAntiquot.parenthesizer :

Parenthesizer

The parenthesizer for LMFDB identifier syntax.

Instances For

source

def Lean.PrettyPrinter.Parenthesizer.pibaseIdAntiquot.parenthesizer :

Parenthesizer

The parenthesizer for π-Base identifier syntax.

Instances For

source

def Lean.PrettyPrinter.Parenthesizer.dlmfIdAntiquot.parenthesizer :

Parenthesizer

The parenthesizer for DLMF identifier syntax.

Instances For

Stacks / Kerodon attribute #

source

def Lean.Parser.Category.stacksTagDB :

Wikidata attribute #

source

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.

Instances For

LMFDB attribute #

source

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.

Instances For

π-Base attribute #

source

def Mathlib.CrossRef.pibaseTopic :

Lean.ParserDescr

The topic identifying a π-Base database. Possible values:

topology

This list will be expanded in the future.

Instances For

source

def Mathlib.CrossRef.getPiBaseTopic? :

Lean.TSyntax `Mathlib.CrossRef.pibaseTopic → Option PiBaseTopic

Get the PiBaseTopic from a syntax key.

Instances For

source

def Mathlib.CrossRef.pibaseTag :

Lean.ParserDescr

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:

topology

This list will be expanded in the future.

The identifier must start with P, S, or T, followed by exactly six digits.

Instances For

DLMF attribute #

source

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.

Instances For

source

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.

Instances For

source

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.

Instances For

source

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.

Instances For

source

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.

Instances For

source

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.

Instances For

source

def Mathlib.CrossRef.pibaseTags :

Lean.ParserDescr

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.

Instances For

source

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.

Instances For

Documentation

Mathlib.Tactic.CrossRefAttribute

Cross-reference attributes #

Stacks (and Kerodon) parser #

Wikidata parser #

LMFDB parser #

π-Base parser #

DLMF parser #

Stacks / Kerodon attribute #

Wikidata attribute #

LMFDB attribute #

π-Base attribute #

DLMF attribute #