Documentation

Mathlib.Util.Imports

Tools for analyzing imports. #

Provides the commands

Find the imports of a given module.

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

    Construct the import graph of the current file.

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

      Return the redundant imports (i.e. those transitively implied by another import) amongst a candidate list of imports.

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

        Compute the transitive closure of an import graph.

        Equations
        Instances For

          Compute the transitive reduction of an import graph.

          Typical usage is transitiveReduction (← importGraph).

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

            Restrict an import graph to only the downstream dependencies of some set of modules.

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

              Restrict an import graph to only the transitive imports of some set of modules.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                partial def Lean.NameMap.transitiveFilteredUpstream (node : Lean.Name) (graph : Lean.NameMap (Array Lean.Name)) (filter : Lean.NameBool) (replacement : optParam (Option Lean.Name) none) :

                Filter the list of edges … → node inside graph by the function filter.

                Any such upstream node source where filter source returns true will be replaced by all its upstream nodes. This results in a list of all unfiltered nodes in the graph that either had an edge to node or had an indirect edge to node going through filtered nodes.

                Will panic if the node is not in the graph.

                Filters the graph removing all nodes where filter n returns false. Additionally, replace edges from removed nodes by all the transitive edges.

                This means there is a path between two nodes in the filtered graph iff there exists such a path in the original graph.

                If the optional (replacement : Name) is provided, a corresponding node will be added together with edges to all nodes which had an incoming edge from any filtered node.

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

                  Return the redundant imports (i.e. those transitively implied by another import) of a specified module (or the current module if none is specified).

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

                    List the imports in this file which can be removed because they are transitively implied by another import.

                    Equations
                    Instances For

                      Return the names of the modules in which constants used in the current file were defined, with modules already transitively imported removed.

                      Note that this will not account for tactics and syntax used in the file, so the results may not suffice as imports.

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

                        Try to compute a minimal set of imports for this file, by analyzing the declarations.

                        This must be run at the end of the file, and is not aware of syntax and tactics, so the results will likely need to be adjusted by hand.

                        Equations
                        Instances For

                          Find locations as high as possible in the import hierarchy where the named declaration could live.

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

                            Find locations as high as possible in the import hierarchy where the named declaration could live. Using #find_home! will forcefully remove the current file. Note that this works best if used in a file with import Mathlib.

                            The current file could still be the only suggestion, even using #find_home! lemma. The reason is that #find_home! scans the import graph below the current file, selects all the files containing declarations appearing in lemma, excluding the current file itself and looks for all least upper bounds of such files.

                            For a simple example, if lemma is in a file importing only A.lean and B.lean and uses one lemma from each, then #find_home! lemma returns the current file.

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