Commit 2021-05-13 20:13 773594c3

View on Github →

feat(Tactic/NormNum): basic normNum from zulip

Estimated changes

Modified Mathlib/Plugin.lean

Created Mathlib/Tactic/NormNum.lean

added theorem Lean.Meta.NormNum.ofNat_add

added theorem Lean.Meta.NormNum.ofNat_mul

added def Lean.Meta.mkOfNatLit

added def Lean.Tactic.evalNormNum