Commit 2023-03-07 23:14 9715cc20

View on Github →

fix: to_additive issue with numerals in constant type family (#2419) Fixes the issue reported here

Estimated changes

Modified Mathlib/Init/ZeroOne.lean

Modified Mathlib/Tactic/NormNum/Basic.lean

Modified Mathlib/Tactic/NormNum/Core.lean

modified def Int.rawCast

modified def Nat.rawCast

modified def Rat.rawCast

Modified Mathlib/Tactic/ToAdditive.lean

deleted def ToAdditive.shouldTranslateNumeral

Modified test/toAdditive.lean

added def Test.fixedNumeralTest2

added def Test.fixedNumeralTest