Lean4
@[tacticAnalysis linter.tacticAnalysis.rwMerge, inherit_doc linter.tacticAnalysis.rwMerge]
def rwMerge : TacticAnalysis.Config :=
.ofComplex
{ out := (List MVarId × Array Syntax)
ctx := (Array (Array Syntax))
trigger ctx
stx :=
match stx with
| `(tactic| rw [$args,*]) => .continue ((ctx.getD #[]).push args)
| _ => if let some args := ctx then if args.size > 1 then .accept args else .skip else .skip
test ctx
goal :=
withOptions (fun opts => opts.set `grind.warning false)
(do
let ctxT : Array (TSyntax `Lean.Parser.Tactic.rwRule) := ctx.flatten.map (⟨·⟩)
let tac ← `(tactic| rw [$ctxT,*])
try
let (goals, _) ← Lean.Elab.runTactic goal tac
return (goals, ctxT.map (↑·))
catch _e => -- rw throws an error if it fails to pattern-match.
return ([goal], ctxT.map (↑·)))
tell _stx _old _oldHeartbeats new
_newHeartbeats := pure <| if new.1.isEmpty then m! "Try this: rw {new.2}" else none }
