Zulip Chat Archive

Stream: new members

Topic: norm_num doesn't prove

Scott Morrison (May 15 2020 at 10:50):

example : 10 = (-1 : ℤ) % 11 :=
by norm_num

Should it?

Reid Barton (May 15 2020 at 10:51):

Is it true?

Reid Barton (May 15 2020 at 10:51):

I guess it has to be true (but it wouldn't be true in C for example)

Jalex Stark (May 15 2020 at 11:39):

#reduce (-1 : ℤ) % 11 gives 10

Jalex Stark (May 15 2020 at 11:41):

example : 10 = (-1 : ℤ) % 11 :=
by refl

example : 10 = (21 : ℤ) % 11 :=
by norm_num

Last updated: Dec 20 2023 at 11:08 UTC