tracking issue for `set_option backward.isDefEq.lazyProjDelta false`
Opened this issue · 0 comments
kim-em commented
This option disables the changes to isDefEq introduced in leanprover/lean4#3965, and is still sometimes necessary in Mathlib.
It would be great to reduce our reliance on this backwards compatibility flag.
This may involve
- just reducing the reliance on defeq in the affected theorems (i.e. more rewrites, less rfl/convert/...)
- producing minimized examples of the places in Mathlib where the old behaviour is required for performance.