installing lean4

Stream: new members

[stewart mandell]

I'm new to everything here, including Tulip. I followed the instructions to install VSCode, lake, and the lean4 extension for VSCode. I make a folder which I see contains the required lake files etc. However when I open Main.lean or MyProject.lean and try to do something as simple as #eval 1 + 1 I get a squiggly line and it doesn't evaluate. I hope someone can get me started, I spent the whole day trying to do this.

[Matt Diamond]

Are you opening the folder in VSCode or just an individual file?

[Matt Diamond]

if it's the latter, try opening the folder instead (use File > Open Folder... instead of File > Open...)

[Notification Bot]

This topic was moved here from #mathlib4 > installing lean4 by Kim Morrison.

[Kim Morrison]

@stewart mandell just pinging you here in case you worry that your message disappeared.

[Kevin Buzzard]

Say which instructions you followed and send a screenshot of VS Code with the file visible and the file explorer open

[stewart mandell]

Going through Mechanics of Proof.

Don't understand what's wrong with my solution to this example

example {n : ℤ} (hn : n ^ 2 + 4 = 4 * n) : n = 2 := by
 have h :=
  calc
  0*(n-2) = n^2- 4*n + 4 := by addarith[hn]
  _= (n-2)*(n-2) := by ring
  cancel (n-2) at h

[Kevin Buzzard]

My guess is that the cancel tactic won't let you cancel x in a hypothesis unless you have a proof that x ≠ 0 (because this would not be valid mathematically) and here you cannot supply that proof because n - 2 = 0 is actually true. In short, you look to me like you're dividing by 0.

[Dan Velleman]

Also, I think you have indented cancel too far--it should be lined up with have, not calc. (Lean can be very fussy about indenting.)