Commit 2020-10-31 20:22 51cbb836

refactor(tactic/norm_num): move norm_num extensions (#4822) #4820 adds the long awaited ability for norm_num to be extended in other files. There are two norm_num extensions currently in mathlib: norm_digits, which was previously exposed as a standalone tactic, and eval_prime, which was a part of norm_num and so caused tactic.norm_num to depend on data.nat.prime. This PR turns both of these into norm_num extensions, and changes the dependencies so that data.nat.prime can import norm_num rather than the other way around (which required splitting pnat primality and gcd facts to their own file).