Commit 2023-01-17 03:10 fc8fc81a

feat: make norm_num erasable (and scoped) (#1364) As per #1308, we give norm_nums the capability to be erased. E.g.

attribute [-norm_num] Mathlib.Meta.NormNum.evalPow

This required us to switch the implementation from a PersistentEnvExtenstion to a ScopedEnvExtension so that the attribute could be erased in a section (or via attribute [-norm_num] ... in) in a way the user would expect. This also easily lets us now make norm_num a localizable attribute. (I imagine that's a rare occurrence, but may as well—the functionality comes for free with ScopedEnvExtension, and all we have to do is not prevent it.) The following explains in detail what changes I make, but the actual changes to the code are small. If you're reviewing this, it might make more sense just to read the code.