Zulip Chat Archive
Stream: new members
Topic: How is 1,2,3 defined in Lean?
YH (Dec 13 2019 at 19:42):
3 is not definitionally equal to succ(2)? I am surprised. How am I supposed to prove 0 < 3 in this case.
Reid Barton (Dec 13 2019 at 19:44):
3 may or may not be definitionally equal to succ 2, depending on what type you are talking about.
Reid Barton (Dec 13 2019 at 19:44):
But the usual answer to the second question is by norm_num.
YH (Dec 13 2019 at 19:45):
Oh great. Thanks.
Last updated: Dec 20 2023 at 11:08 UTC