Def ToAdditive.copySimpAttribute

Modification history

2023-01-09 17:24

Mathlib/Tactic/ToAdditive.lean

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

Deleted ToAdditive.copySimpAttribute View on Github →

2022-12-06 06:42

Mathlib/Tactic/ToAdditive.lean

chore: copy `norm_cast` attributes in `to_additive` (#847)

Modified ToAdditive.copySimpAttribute View on Github →

2022-11-24 02:16

Mathlib/Tactic/ToAdditive.lean

chore: to_additive adds instances (#678)

Added ToAdditive.copySimpAttribute View on Github →