Def ToAdditive.shouldTranslateNumeral

Modification history

2023-03-07 23:14
Mathlib/Tactic/ToAdditive.lean
fix: to_additive issue with numerals in constant type family (#2419) …
Deleted ToAdditive.shouldTranslateNumeralView on Github →
2023-01-17 03:10
Mathlib/Tactic/ToAdditive.lean
feat: remove replaceAll option from to_additive (#1504) …
Modified ToAdditive.shouldTranslateNumeralView on Github →
2022-12-16 09:48
Mathlib/Tactic/ToAdditive.lean
perf: improve to_additive performance (#1060) …
Modified ToAdditive.shouldTranslateNumeralView on Github →
2022-11-24 01:53
Mathlib/Tactic/ToAdditive.lean
fix: fix to_additive handling of Nat and Int (#689) …
Added ToAdditive.shouldTranslateNumeralView on Github →