Zulip Chat Archive

Stream: new members

Topic: typo in exercise 4.3?

Óscar Martín (Oct 24 2021 at 11:54):

Hi, it seems to me that exercise 3 in chapter 4 (on barber's paradox) should read

example (h :  x : men, shaves barber x  ¬ shaves x x) : False := sorry

with a capital F in False. Right? I'm only able to prove it this way. Anyway, I'm a complete newbie on Lean (and enjoying it :-)) so, if I'm wrong, I would appreciate an explanation.

Reid Barton (Oct 24 2021 at 11:55):

Are you using Lean 4?

Óscar Martín (Oct 24 2021 at 11:57):

Yes, I am.

Reid Barton (Oct 24 2021 at 11:58):

I guess my first question should have been: is the book you're following for Lean 4? If so then it's probably a typo.

Óscar Martín (Oct 24 2021 at 12:06):

Yeah, this one: https://leanprover.github.io/theorem_proving_in_lean4/

Óscar Martín (Oct 24 2021 at 12:07):

These exercises: https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#exercises

Kevin Buzzard (Oct 24 2021 at 14:08):

Yes that sounds right. This book has only recently been ported to lean 4 so this might not be the only typo. @Jeremy Avigad are you in charge of this version or is it sometime else needs pinging?

Patrick Massot (Oct 24 2021 at 14:14):

Jeremy wasn't involved in the port

Jeremy Avigad (Oct 24 2021 at 15:05):

But I just fixed it. @Óscar Martín, thank you for the the correction.

Óscar Martín (Oct 24 2021 at 15:56):

Let's call it my very small contribution to Lean :-)
Thank you all for your work.

Last updated: Dec 20 2023 at 11:08 UTC