Commit 2024-04-12 13:24 3469775e

View on Github →

fix: make sure tactics in DefEqTransformations do not reorder hypotheses (#12077) Reported by Damiano Testa on Zulip. The upstream function Lean.MVarId.changeLocalDecl should probably be changed to preserve hypothesis order, but for now we add the Lean.MVarId.changeLocalDecl' variant.

Estimated changes

Modified Mathlib/Tactic/DefEqTransformations.lean

added def Lean.MVarId.changeLocalDecl'

Modified test/DefEqTransformations.lean