Def ToAdditive.nameDict

Modification history

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