Def Mathlib.Tactic.evalGRewriteSeq

Modification history

2026-04-29 09:12
Mathlib/Tactic/GRewrite/Elab.lean
chore(GRewrite): copy how `rw` elaborates (#38558) …
Deleted Mathlib.Tactic.evalGRewriteSeqView on Github →
2025-06-11 22:43
Mathlib/Tactic/GRewrite/Elab.lean
feat: a `grw` tactic for rewriting using inequalities (#8167)
Added Mathlib.Tactic.evalGRewriteSeqView on Github →