Zulip Chat Archive

Stream: new members

Topic: norm_num doesn't prove


view this post on Zulip Scott Morrison (May 15 2020 at 10:50):

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

Should it?

view this post on Zulip Reid Barton (May 15 2020 at 10:51):

Is it true?

view this post on Zulip 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)

view this post on Zulip Jalex Stark (May 15 2020 at 11:39):

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

view this post on Zulip Jalex Stark (May 15 2020 at 11:41):

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

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

Last updated: May 06 2021 at 21:09 UTC