Commit 2024-07-15 23:26 1f66a3e7
View on Github →feat(to_additive): unfold lemmas generated by simp (#14628)
- This removes a bunch of hacky code
- Thanks to @kmill for the idea
- Also fix a bug in the implementation of
@[to_additive (attr := to_additive, x)] - The removed test tested for an implementation detail. The rest of the test file (and Mathlib) still passes, which shows that it still works as desired.