good tutorial for vscode + lean in windows

Stream: new members

[Piero Giacomelli]

Dear all, I am struggling to understand how to make VSCODE working correctly with lean in windows. Can someone point me to a clear tutorial I tried GOOGLING but still had some issue. Any help is appreciated

[Henrik Böving]

Usually we just install the Lean 4 extension through the official vscode store and it just works. If you are experiencing issues while doing that or have an issue after the installation process please give us additional information on what you are doing.

[Marc Huisinga]

Specifically, you should be able to follow https://lean-lang.org/lean4/doc/quickstart.html to install Lean 4 with VS Code

[Piero Giacomelli]

Marc Huisinga said:

Specifically, you should be able to follow https://lean-lang.org/lean4/doc/quickstart.html to install Lean 4 with VS Code

many thanks @Marc Huisinga I was finally able to setup the thing! I am starting the learning path