NNG4 in vscode

Stream: new members

[Eduardo Cavazos]

Hello!

Level 8/8 of NNG4 is where we prove that 2+2=4.

Here's one solution:

nth_rewrite 2 [two_eq_succ_one]
rw [add_succ]
rw [one_eq_succ_zero]
rw [add_succ]
rw [add_zero]
rw [← three_eq_succ_two]
rw [← four_eq_succ_three]
rfl

If I go to editor mode, I can experiment with the solution there:

image.png

Question

Is there a way to run this solution in vscode?

I cloned the NNG4 repository:

https://github.com/leanprover-community/NNG4

When I try to use two_eq_succ_one I get the following:

image.png

I imagine I'll need some additional import lines.

My test file bcd.lean is in:

C:\temp\NNG4\Game\bcd.lean

I.e. I placed it in the github repository with the intention that it can see the NNG4 files.

Note that I'm not looking to run the web version locally.
I'd just like to run some of the NNG4 solutions locally in vscode.

Any suggestions are welcome.

Thanks!

[Kevin Buzzard]

Yeah you can totally do this, this is how I make the levels myself. I would import the actual level: import Game.Levels.Tutorial.L08twoaddtwo to make sure everything is there, and then I would write namespace MyNat and hopefully this solves your problems.

[Eduardo Cavazos]

That works perfectly.

Thanks so much @Kevin Buzzard!

For reference for others, here's the exact text I used for that level in vscode:

-- https://adam.math.hhu.de/#/g/leanprover-community/nng4/world/Tutorial/level/8

import Game.Levels.Tutorial.L08twoaddtwo

namespace MyNat

example : (2 : ℕ) + 2 = 4 := by
  nth_rewrite 2 [two_eq_succ_one]
  rw [add_succ]
  rw [one_eq_succ_zero]
  rw [add_succ]
  rw [add_zero]
  rw [← three_eq_succ_two]
  rw [← four_eq_succ_three]
  rfl

Here's what it looks like in vscode:

image.png