Def ToAdditive.addToAdditiveAttr
Modification history
2023-02-17 17:10
Mathlib/Tactic/ToAdditive.lean
feat: to_additive raises linter errors; nested to_additive (#1819) …
Deleted ToAdditive.addToAdditiveAttrView on Github →2022-12-01 21:40
Mathlib/Tactic/ToAdditive.lean
feat: show info on to_additive even if the declaration already exists (#816) …
Modified ToAdditive.addToAdditiveAttrView on Github →