Def ToAdditive.proceedFieldsAux

Modification history

2023-02-03 22:53
Mathlib/Tactic/ToAdditive.lean
refactor: change the way to_additive parses options (#1780) …
Added ToAdditive.proceedFieldsAuxView on Github →