Commit 2023-05-23 04:50 6292b8e9

View on Github →

feat: norm num extension for division and succ of naturals (#4090)

Estimated changes

Modified Mathlib/Tactic/NormNum/Basic.lean

added def Mathlib.Meta.NormNum.evalNatDiv

added def Mathlib.Meta.NormNum.evalNatSucc

added theorem Mathlib.Meta.NormNum.isNat_natDiv

added theorem Mathlib.Meta.NormNum.isNat_natSucc

Modified test/norm_num.lean