Lean4
/-- `#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.
-/
@[command_parser 1000]
public meta def transImportsStx : Lean.ParserDescr✝ :=
ParserDescr.node✝ `transImportsStx 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "#trans_imports")
(ParserDescr.unary✝ `optional
(ParserDescr.binary✝ `andthen (ParserDescr.const✝ `ppSpace) (ParserDescr.const✝ `str))))
(ParserDescr.unary✝ `optional
(ParserDescr.binary✝ `andthen ((with_annotate_term"&" @ParserDescr.nonReservedSymbol✝) " at_most " false✝)
(ParserDescr.const✝ `num))))
