Lim, Thing-han (Feb 24 2021 at 08:26):
I followed the instructions of the lean4 viscose extensions, run
npm install then open VS Code on the folder, then Press
Ctrl + Shift + B to compile.
However it then reports
Error: Can't resolve './src/extension.ts'.
Do I misunderstand something? how can I setup the vscode extension?
Sebastian Ullrich (Feb 24 2021 at 08:57):
You should get the extension from the marketplace if you're not interested in extending it
Marc Huisinga (Feb 24 2021 at 09:34):
Or open the extensions menu on the left in VSCode and type in
lean4, then install the extension.
Last updated: May 07 2021 at 11:09 UTC