#show_imports for <cmd>

This module provides the simple command #show_imports for <cmd> which shows a minimal set of imports needed to elaborate <cmd>, including the import needs of the declarations produced during that command, any prior declarations from the same file, and the syntax of the command.

Note that this currently does not work for example.

Future work

• Better attribution of import needs to declarations/syntax/etc.

def ImportGraph.Shake.«command#show_imports_For__» : Lean.ParserDescr

#show_imports for <cmd> shows a minimal set of imports needed by <cmd>. This includes

• The import needs of any declarations elaborated in the command
• The import needs of any previously-defined constants from the same file used in those declarations
• The syntax needs of the current command (but not the syntax needs of same-file dependencies of constants produced in the command, which we do not have access to)
• Any extra shake records produced by the command. (These may be due to syntax, tactics, etc.)

The imports may be copied by clicking the "copy" icon.

Equations

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