Commit 2020-05-15 13:15 471d29e8

View on Github →

perf(tactic/ring): use new norm_num, avoid mk_app (#2685) Remove tactic.norm_num from ring, and do some performance upgrades borrowed from the norm_num overhaul while I'm at it.

Estimated changes

Modified src/tactic/norm_num.lean

Modified src/tactic/ring.lean

modified theorem tactic.ring.horner_pow

added theorem tactic.ring.pow_succ

Modified test/ring.lean