Lean4
/-- The `convert_to` tactic is for changing the type of the target or a local hypothesis,
but unlike the `change` tactic it will generate equality proof obligations using `congr!`
to resolve discrepancies.
* `convert_to ty` changes the target to `ty`
* `convert_to ty using n` uses `congr! n` instead of `congr! 1`
* `convert_to ty at h` changes the type of the local hypothesis `h` to `ty`.
Any remaining `congr!` goals come first.
Operating on the target, the tactic `convert_to ty using n`
is the same as `convert (?_ : ty) using n`.
The difference is that `convert_to` takes a type but `convert` takes a proof term.
Except for it also being able to operate on local hypotheses,
the syntax for `convert_to` is the same as for `convert`, and it has variations such as
`convert_to ← g` and `convert_to (config := {transparency := .default}) g`.
Note that `convert_to ty at h` may leave a copy of `h` if a later local hypotheses or the target
depends on it, just like in `rw` or `simp`.
-/
@[tactic_parser 1000]
public meta def convertTo : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.convertTo 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "convert_to" false✝)
(ParserDescr.unary✝ `optional Lean.Parser.Tactic.config))
(ParserDescr.unary✝ `optional (ParserDescr.symbol✝ " ←")))
(ParserDescr.const✝ `ppSpace))
(ParserDescr.cat✝ `term 0))
(ParserDescr.unary✝ `optional
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " using ") (ParserDescr.const✝ `num))))
(ParserDescr.unary✝ `optional
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " with")
(ParserDescr.unary✝ `many
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.const✝ `ppSpace) (ParserDescr.const✝ `colGt))
(ParserDescr.cat✝ `rintroPat 0))))))
(ParserDescr.unary✝ `optional Lean.Parser.Tactic.location))
