Def ToAdditive.setInlineAttribute

Modification history

2025-04-02 12:42
Mathlib/Tactic/ToAdditive/Frontend.lean
fix: have `to_additive` unfold aux lemmas before translation (#23559) …
Deleted ToAdditive.setInlineAttributeView on Github →
2024-08-08 20:12
Mathlib/Tactic/ToAdditive/Frontend.lean
fix: make `to_additive` deal with `abbrev` correctly (#15474)
Added ToAdditive.setInlineAttributeView on Github →