Lean4
/-- Writing
```lean
deprecate to new_name new_name₂ ... new_nameₙ
theorem old_name : True := .intro
```
where `new_name new_name₂ ... new_nameₙ` is a sequence of identifiers produces the
`Try this` suggestion:
```lean
theorem new_name : True := .intro
@[deprecated (since := "YYYY-MM-DD")] alias old_name := new_name
@[deprecated (since := "YYYY-MM-DD")] alias old_name₂ := new_name₂
...
@[deprecated (since := "YYYY-MM-DD")] alias old_nameₙ := new_nameₙ
```
where `old_name old_name₂ ... old_nameₙ` are the non-blacklisted declarations
(auto)generated by the initial command.
The "YYYY-MM-DD" entry is today's date and it is automatically filled in.
`deprecate to` makes an effort to match `old_name`, the "visible" name, with
`new_name`, the first identifier produced by the user.
The "old", autogenerated declarations `old_name₂ ... old_nameₙ` are retrieved in alphabetical order.
In the case in which the initial declaration produces at most 1 non-blacklisted
declarations besides itself, the alphabetical sorting is irrelevant.
Technically, the command also take an optional `String` argument to fill in the date in `since`.
However, its use is mostly intended for debugging purposes, where having a variable date would
make tests time-dependent.
-/
@[command_parser 1000]
public meta def commandDeprecateTo______ : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.DeprecateTo.commandDeprecateTo______ 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "deprecate") (ParserDescr.symbol✝ "to"))
(ParserDescr.unary✝ `many (ParserDescr.const✝ `ident)))
(ParserDescr.unary✝ `optional
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.const✝ `ppSpace) (ParserDescr.const✝ `str))
(ParserDescr.const✝ `ppSpace))))
(ParserDescr.unary✝ `group (ParserDescr.const✝ `ppLine)))
(ParserDescr.cat✝ `command 0))
