Installing Lean 4 M2 Mac

Stream: new members

[Riyaz Ahuja]

Hi all, I'm super new to lean, and I've been working on it using the online editor. I want to use vscode now, and I followed the instructions on the site to download lean 4 for macs, but now when I do a small test program in my vscode, I get a weird error:

example (p q : Prop) : p ∧ q → q ∧ p :=
  intro h

Where the error is that there is an unknown identifier "intro". Obviously, intro is a valid identifier, so I'm assuming I installed it wrong. How can I troubleshoot and fix this. Sorry if this is a repeat of an often asked question!

[Damiano Testa]

You should place a by to "start tactic mode".

[Damiano Testa]

example (p q : Prop) : p ∧ q → q ∧ p := by -- <--  here!
  intro h

[Damiano Testa]

(Without by Lean is by default in term mode: it does not accept tactics, but directly the proof term.)