fix: use `Expr.equal` instead of `==` in `MVarId.replaceTargetDefEq` and `MVarId.replaceLocalDeclDefEq`

leanprover / lean4

Lean 4 programming language and theorem prover

https://lean-lang.org

Apache License 2.0

4.74k stars 427 forks source link

fix: use `Expr.equal` instead of `==` in `MVarId.replaceTargetDefEq` and `MVarId.replaceLocalDeclDefEq` #6098

Closed kmill closed 1 week ago

kmill commented 1 week ago

This PR modifies Lean.MVarId.replaceTargetDefEq and Lean.MVarId.replaceLocalDeclDefEq to use Expr.equal instead of Expr.eqv when determining whether the expression has changed. This is justified on the grounds that binder names and binder infos are user-visible and affect elaboration.

leanprover-community-bot commented 1 week ago

Mathlib CI status (docs):

✅ Mathlib branch lean-pr-testing-6098 has successfully built against this PR. (2024-11-16 01:59:11) View Log