Documentation

Mathlib.Tactic.StacksAttribute

The stacks and kerodon attributes #

This allows tagging of mathlib results with the corresponding tags from the Stacks Project and Kerodon.

While the Stacks Project is the main focus, because the tag format at Kerodon is compatible, the attribute can be used to tag results with Kerodon tags as well.

Web database users of projects tags

Instances For

    Tag is the structure that carries the data of a project tag and a corresponding Mathlib declaration.

    • declName : Lean.Name

      The name of the declaration with the given tag.

    • database : Database

      The online database where the tag is found.

    • tag : String

      The database tag.

    • comment : String

      The (optional) comment that comes with the given tag.

    Instances For

      Defines the tagExt extension for adding a HashSet of Tags to the environment.

      def Mathlib.StacksTag.addTagEntry {m : TypeType} [Lean.MonadEnv m] (declName : Lean.Name) (db : Database) (tag comment : String) :

      addTagEntry declName tag comment takes as input the Name declName of a declaration and the Strings tag and comment of the stacks attribute. It extends the Tag environment extension with the data declName, tag, comment.

      Equations
        Instances For
          @[reducible, inline]

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

          Equations
            Instances For

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

              Equations
                Instances For

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

                  Equations
                    Instances For

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

                      Equations
                        Instances For

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

                          Equations
                            Instances For

                              The formatter for Stacks Project Tags syntax.

                              Equations
                                Instances For

                                  The parenthesizer for Stacks Project Tags syntax.

                                  Equations
                                    Instances For

                                      The syntax category for the database name.

                                      Equations
                                        Instances For

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

                                          Equations
                                            Instances For

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

                                              Equations
                                                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
                                                    Instances For

                                                      traceStacksTags db verbose prints the tags of the database db to the user and inlines the theorem statements if verbose is true.

                                                      Equations
                                                        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 after each summary line.

                                                          Equations
                                                            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 after each summary line.

                                                              Equations
                                                                Instances For