Installing Lean 4

Stream: new members

[Emilie Uthaiwat]

Hello,

After installing Lean 4, I tried to open the Infoview but it does not work anymore. When I click on it, I get the following error message:

command 'lean4.displayGoal' not found

Could someone please help me solve this problem? Please find below a screenshot of VS Code:
screenshot.PNG

[Arthur Paulino]

You need to open VS Code in the Lean 4 project folder

[Arthur Paulino]

I think you're like 2 levels higher than you should

[Emilie Uthaiwat]

I switched to the Lean 4 project folder and the Infoview now works. Thank you!