max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: quickstart: beware the Windows

Browse source
This commit is contained in:
Sebastian Ullrich 2021-04-07 14:50:36 +02:00
parent 4517c518c8
commit 7de11d2aa3
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
doc/quickstart.md
View file

@ -8,6 +8,7 @@ See [Setup](./setup.md) for other ways and more details on setting up Lean.
$ curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain leanprover/lean4:nightly
```
See the `elan` link above for other installation options and details.
Note that using Lean with multi-file projects on Windows currently comes with some [additional limitations](./setup.md#leanpkg).
1. Install [VS Code](https://code.visualstudio.com/).
1. Open VS Code and install the `lean4` extension.
![installing the vscode-lean4 extension](images/code-ext.png)