Zulip Chat Archive

Stream: maths

Topic: literals in int

Jakob von Raumer (Feb 13 2023 at 11:06):

What's the efficient way to prove -(361850278866613121369732278309507010562310721533159669997309205613587202 : ℤ) = -361850278866613121369732278309507010562310721533159669997309205613587202?

Kevin Buzzard (Feb 13 2023 at 11:14):

What does norm_num do? Is this lean 3 or lean 4?

Riccardo Brasca (Feb 13 2023 at 11:20):

Does rfl work?

Jakob von Raumer (Feb 13 2023 at 11:21):

Kevin Buzzard said:

What does norm_num do? Is this lean 3 or lean 4?

Lean 3 (yes, maybe I should port that stuff instead). So simp does it, but it does the logarithmic bit0 and bit1 which seems unnecessary.

Jakob von Raumer (Feb 13 2023 at 11:21):

Riccardo Brasca said:

Does rfl work?

Nope

Riccardo Brasca (Feb 13 2023 at 11:24):

This works for me

example (n : ℕ) : -(n : ℤ) = -n := rfl

So you can name it and use it for any number you want.

Riccardo Brasca (Feb 13 2023 at 11:26):

Mmh, no, it doesn't

Reid Barton (Feb 13 2023 at 11:26):

I think the original question is not well posed: when I replace the number by a smaller one, the two sides are syntactically identical.

Riccardo Brasca (Feb 13 2023 at 11:28):

Ah yes, rfl works for me

Last updated: Dec 20 2023 at 11:08 UTC