Lean4
/-- `rewrite!` is like `rewrite`,
but can also insert casts to adjust types that depend on the LHS of a rewrite.
It is available as an ordinary tactic and a `conv` tactic.
The sort of casts that are inserted is controlled by the `castMode` configuration option.
By default, only proof terms are casted;
by proof irrelevance, this adds no observable complexity.
With `rewrite! +letAbs (castMode := .all)`, casts are inserted whenever necessary.
This means that the 'motive is not type correct' error never occurs,
at the expense of creating potentially complicated terms.
-/
@[tactic_parser 1000]
public meta def depRewriteSeq : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.DepRewrite.depRewriteSeq 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "rewrite!" false✝) Lean.Parser.Tactic.optConfig)
Lean.Parser.Tactic.rwRuleSeq)
(ParserDescr.unary✝ `optional Lean.Parser.Tactic.location))
