Commit 2021-08-18 00:45 05b74b09

View on Github →

fix(Tactic/NormNum): fix normNum bug Reported on zulip. Also some minor cleanup of normNum and ring.

Estimated changes

Created Mathlib/Tactic/Core.lean

added def Lean.Expr.getAppFnArgs

added def Lean.Expr.natLit!

Modified Mathlib/Tactic/NormNum.lean

added def Lean.Meta.NormNum.eval

added theorem Lean.Meta.NormNum.ofNat_nat

Modified Mathlib/Tactic/Ring.lean

deleted def Lean.Expr.getAppFnAndArgs

modified def Tactic.Ring.HornerExpr.pp

added def Tactic.Ring.RingM.run

deleted def Tactic.Ring.run