Commit 2024-08-08 20:12 a951fed0

View on Github →

fix: make to_additive deal with abbrev correctly (#15474)

Estimated changes

Modified Mathlib/Tactic/ToAdditive/Frontend.lean

added def ToAdditive.setInlineAttribute

Modified test/toAdditive.lean