Commit 2020-05-09 20:30 b7698468

feat(tactic/norm_num): new all-lean norm_num (#2589) This is a first draft of the lean replacement for tactic.norm_num in core. This isn't completely polished yet; the rest of norm_num can now be a little less "global-recursive" since the primitives for e.g. adding and multiplying natural numbers are exposed. I'm also trying out a new approach using functions like match_neg and match_numeral instead of directly pattern matching on exprs, because this generates smaller (and hopefully more efficient) code. (Without this, some of the matches were hitting the equation compiler depth limit.) I'm open to new feature suggestions as well here. nat.succ and coercions seem useful to support in the core part, and additional flexibility using def_replacer is also on the agenda.