Structure ToAdditive.ValueType

Modification history

2022-12-01 21:40

Mathlib/Tactic/ToAdditive.lean

feat: show info on to_additive even if the declaration already exists (#816) …

Deleted ToAdditive.ValueType View on Github →

2022-05-11 23:41

Mathlib/Tactic/ToAdditive.lean

feat: `to_additive` (#234) …

Added ToAdditive.ValueType View on Github →