The #trans_imports command

#trans_imports reports how many transitive imports the current module has. The command takes an optional string input: #trans_imports str also shows the transitively imported modules whose name begins with str.

def transImportsStx : Lean.ParserDescr

#trans_imports reports how many transitive imports the current module has. The command takes an optional string input: #trans_imports str also shows the transitively imported modules whose name begins with str.

Mostly for the sake of tests, the command also takes an optional at_most x input: if the number of imports does not exceed x, then the message involves x, rather than the actual, possibly varying, number of imports.

Equations

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