Def ToAdditive.proceedFieldsAux

Modification history

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 →