Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
chore: rw? uses MVarId.refl not MVarId.applyRfl (#3783)
I think this was in error in my original Mathlib implementation. We're not interested in relations other than `=`, so there is no point uses `MVarId.applyRfl`, which just looks up `@[refl]` tagged lemmas and tries those. In a separate PR, I will change `MVarId.applyRfl` so it has a flag to control whether on `=` it should just hand-off to `MVarId.refl`, or fail. Failure is appropriate in the version we call from the `rfl` macro, to avoid doing a double `IsDefEq` check on every `rfl`!
- Loading branch information