Zulip Chat Archive

Stream: general

Topic: Not expected behavior using norm_num


view this post on Zulip Bruno Bentzen (Dec 21 2018 at 02:02):

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

view this post on Zulip Bryan Gin-ge Chen (Dec 21 2018 at 02:08):

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

view this post on Zulip Mario Carneiro (Dec 21 2018 at 02:12):

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

view this post on Zulip Mario Carneiro (Dec 21 2018 at 02:13):

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

view this post on Zulip Bryan Gin-ge Chen (Dec 21 2018 at 02:13):

Oh, is this the 3.4.1 branch issue again?

view this post on Zulip Mario Carneiro (Dec 21 2018 at 02:13):

oh, that might be it

view this post on Zulip Mario Carneiro (Dec 21 2018 at 02:15):

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

view this post on Zulip Bruno Bentzen (Dec 21 2018 at 02:15):

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

view this post on Zulip Bruno Bentzen (Dec 21 2018 at 02:21):

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

view this post on Zulip Bruno Bentzen (Dec 21 2018 at 02:59):

It works now. Thanks, Bryan and Mario!


Last updated: May 13 2021 at 04:21 UTC