mathlib

9cb7e937 - feat(tactic/norm_num): permit disabling the calculation of `/`, `%`, `∣` (#16588)

feat(tactic/norm_num): permit disabling the calculation of `/`, `%`, `∣` (#16588) For teaching, I would like to be able to turn off `norm_num`'s power to calculate `/`, `%`, `∣`. This can be achieved by moving `norm_num.eval_nat_succ_ext` from the core tactic to an extension, so that it can be locally disabled with ```lean local attribute [-norm_num] norm_num.eval_nat_int_ext ``` (Interested users: note that this is only useful if you also make `int.has_div`, `nat.has_dvd`, etc irreducible with ```lean local attribute [irreducible] int.has_div nat.has_dvd ... ``` since otherwise many of these goals can be solved by `refl`.) Zulip: https://leanprover.zulipchat.com/#narrow/stream/239415-metaprogramming-.2F-tactics/topic/Selectively.20weaken.20norm_num