Def ToAdditive.proceedFieldsAux

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.proceedFieldsAux View on Github →

2024-12-21 23:59

Mathlib/Tactic/ToAdditive/Frontend.lean

fix(to_additive): automatically translate all instances generated by `extends` (#19302) …

Modified ToAdditive.proceedFieldsAux View on Github →

2023-02-03 22:53

Mathlib/Tactic/ToAdditive.lean

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

Added ToAdditive.proceedFieldsAux View on Github →