Commit 2023-02-02 19:53 60790d4f

View on Github →

norm_num nat subtraction (#1997) Implements #1899!

Estimated changes

Modified Mathlib/Tactic/NormNum/Basic.lean

added def Mathlib.Meta.NormNum.evalNatSub

added theorem Mathlib.Meta.NormNum.isNat_natSub

Modified Mathlib/Tactic/NormNum/Core.lean

Modified test/norm_num.lean