Commit 2022-12-06 23:13 213105f2
View on Github →fix: removed (incorrect) test for symm, trans attributes (#857)
Fixes error I made: introducing a test for symm
and trans
attributes to check that the lemmas were "genuinely" symm/trans lemmas. However the tests had false positives, e.g. #855 (which has been added to the tests).
This short commit removes the tests. They were not present in mathlib3
anyway and the worst that happens if a lemma is incorrectly labelled is that the symm
tactic tries and fails with this.
As a warning it may be useful to have a test, but it should have no false positives. For now it seems the best approach is to drop the test.