Def ToAdditive.copyMetaData

Modification history

2023-02-17 17:10

Mathlib/Tactic/ToAdditive.lean

feat: to_additive raises linter errors; nested to_additive (#1819) …

Deleted ToAdditive.copyMetaData View on Github →

2023-01-09 17:24

Mathlib/Tactic/ToAdditive.lean

feat: improve the way to_additive deals with attributes (#1314) …

Modified ToAdditive.copyMetaData View on Github →

2022-12-16 04:08

Mathlib/Tactic/ToAdditive.lean

fix: two to_additive changes (#1057) …

Added ToAdditive.copyMetaData View on Github →