Commit 2022-12-03 00:16 2b51fb7f

View on Github →

feat: port nth_rewrite (#823) We just use features that are already in core. The implementation of Occurrences seems to be better than in Lean 3.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Mathport/Syntax.lean

Created Mathlib/Tactic/NthRewrite.lean

added def Mathlib.Tactic.evalNthRewriteSeq

added def Mathlib.Tactic.rewriteLocalDecl'

added def Mathlib.Tactic.rewriteTarget'

Created test/NthRewrite.lean