typo in exercise 4.3?

Stream: new members

[Óscar Martín]

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]

Are you using Lean 4?

[Óscar Martín]

Yes, I am.

[Reid Barton]

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]

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

[Óscar Martín]

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

[Kevin Buzzard]

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]

Jeremy wasn't involved in the port

[Jeremy Avigad]

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

[Óscar Martín]

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