Not expected behavior using norm_num

Stream: general

[Bruno Bentzen]

Hi everyone,

I have a bare project (with mathlib imported) in which the following code

import data.nat.prime  tactic.norm_num

lemma prime_seven : nat.prime (7 : ℕ) := by
norm_num

displays the error 'norm_num failed to simplify'. Does it work for you?

Best,
Bruno

[Bryan Gin-ge Chen]

I get no errors on my system. What version of mathlib are you using? Do other primes like 2, 3 work?

[Mario Carneiro]

If you click on norm_num to go to the definition, search in that file for a function called eval_prime

[Mario Carneiro]

If you don't have it, chances are you are running an old version of mathlib

[Bryan Gin-ge Chen]

Oh, is this the 3.4.1 branch issue again?

[Mario Carneiro]

oh, that might be it

[Mario Carneiro]

go into _target/deps/mathlib and git checkout master then lean --make (which will take a while)

[Bruno Bentzen]

yeah, no eval_prime. Then I should be really using an old version of it.

[Bruno Bentzen]

Thanks! I'm fixing the build, I think it should work now.

[Bruno Bentzen]

It works now. Thanks, Bryan and Mario!