Def ToAdditive.elabToAdditive

Modification history

2025-08-12 21:40

Mathlib/Tactic/ToAdditive/Frontend.lean

feat: deprecate `str` syntax for `to_additive` docstrings in Mathlib (#28135) …

Deleted ToAdditive.elabToAdditive View on Github →

2023-02-03 22:53

Mathlib/Tactic/ToAdditive.lean

refactor: change the way to_additive parses options (#1780) …

Added ToAdditive.elabToAdditive View on Github →