Documentation

Mathlib.Tactic.CrossRefAttribute

Cross-reference attributes #

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

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.Database :
Type

The supported external databases

Instances For
    source
    def Mathlib.CrossRef.instBEqDatabase.beq :
    Database → Database → Bool
    Instances For
      source
      @[implicit_reducible]
      instance Mathlib.CrossRef.instBEqDatabase :
      BEq Database
      source
      def Mathlib.CrossRef.instHashableDatabase.hash :
      Database → UInt64
      Instances For
        source
        @[implicit_reducible]
        instance Mathlib.CrossRef.instHashableDatabase :
        Hashable Database
        source
        def Mathlib.CrossRef.databaseURL :
        Database → String

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

        Instances For
          source
          def Mathlib.CrossRef.databaseLabel :
          Database → String

          The display label used in docstring links and trace output.

          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
              @[implicit_reducible]
              instance Mathlib.CrossRef.instBEqTag :
              BEq Tag
              source
              def Mathlib.CrossRef.instBEqTag.beq :
              Tag → Tag → Bool
              Instances For
                source
                @[implicit_reducible]
                instance Mathlib.CrossRef.instHashableTag :
                Hashable Tag
                source
                def Mathlib.CrossRef.instHashableTag.hash :
                Tag → UInt64
                Instances For
                  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
                                      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.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.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

                                                  Stacks / Kerodon attribute #

                                                  source
                                                  def Lean.Parser.Category.stacksTagDB :
                                                  Category

                                                  The syntax category for the database name.

                                                  Instances For
                                                    source
                                                    def Mathlib.CrossRef.stacksTagDB.quot :
                                                    Lean.ParserDescr
                                                    Instances For
                                                      source
                                                      def Mathlib.CrossRef.stacksTagDBKerodon :
                                                      Lean.ParserDescr

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

                                                      Instances For
                                                        source
                                                        def Mathlib.CrossRef.stacksTagDBStacks :
                                                        Lean.ParserDescr

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

                                                        Instances For
                                                          source
                                                          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.

                                                          Instances For

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