Error on Lean Live using inductive definitions

Stream: general

[Matheus Andrade]

Hello! Sorry if this is the wrong stream to post this question but I'm new to Zulip and Lean.
Right now I'm getting into Lean and trying to define my own booleans and their operators, then show theorems about it.
In Functional Programming in Lean section 1.5 they show a definition for Bool using the pattern inductive Bool where....
I tried defining Bool like that in Lean Live but I get the error invalid binder declaration, delimiter/bracket expected (i.e., '(', '{', '[', '{{').
What did I do wrong? How do I fix this?
I tried changing the words Bool to Cool, true to crue etc as to avoid any sort of conflict with some standard Bool, but the error persists.
Thanks in advance.

[Alex J. Best]

I believe the FPIL book is about lean 4 and the live web editor you linked to runs lean 3 right now.
Do you know which version you would like to start learning? Lean 4 is only in pre-release at this stage, but is already very advanced for programming with. It just doesnt have a large library of mathematics ported yet. The syntax is broadly similar, but as you see there are some differences.

[Matheus Andrade]

Thanks for the answer! I was planning on using Functional Programming in Lean, Theorem Proving in Lean, Logic and Proof and the Lean reference manual as study material. Are those written for Lean 4 too?
Edit: Is there a command that outputs the Lean version? I looked for something like that in Lean Live with no success.

[Kevin Buzzard]

FPIL is 4, LaP is 3 (unless it was updated since I last looked) and TPIL is both.

[Matheus Andrade]

I guess I'm going for Lean4 then. Thanks a lot for the answers!