Lean4
/-- `deprecated_module "Optional string" (since := "yyyy-mm-dd")` deprecates the current module `A`
in favour of its direct imports.
This means that any file that directly imports `A` will get a notification on the `import A` line
suggesting to instead import the *direct imports* of `A`.
-/
@[command_parser 1000]
public meta def deprecated_modules : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Linter.deprecated_modules 1024
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "deprecated_module ")
(ParserDescr.unary✝ `optional
(ParserDescr.binary✝ `andthen (ParserDescr.const✝ `str) (ParserDescr.const✝ `ppSpace))))
(ParserDescr.symbol✝ "("))
((with_annotate_term"&" @ParserDescr.nonReservedSymbol✝) "since " false✝))
(ParserDescr.symbol✝ ":= "))
(ParserDescr.const✝ `str))
(ParserDescr.symbol✝ ")"))
