Selectively weaken norm_num

Stream: metaprogramming / tactics

[Heather Macbeth]

For teaching, I'd like to have a version of norm_num which doesn't have the power to do elementary number theory calculations like a % b or a ∣ b.

It seems to me that I could get this functionality by de-listing eval_nat_int_ext from the main norm_num instructions, and instead making eval_nat_int_ext a norm_num plugin by marking it with the attribute @[norm_num]. Then, in the files when I want to disable the functionality, I could say

local attribute [-norm_num] eval_nat_int_ext

Will my plan work? Would it be the right way to achieve my goal? And would it be acceptable in mathlib?

[Mario Carneiro]

Have you checked if that actually works? I suspect that you can't actually disable the @[norm_num] attribute

[Heather Macbeth]

Right, I haven't tried it. I'll try it later. If it doesn't work, can you suggest another mechanism?

[Heather Macbeth]

@Mario Carneiro Actually, this seems to work just fine! See #16588.