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

doc: quickstart note on moving from Lean 3 to 4

Browse source
This commit is contained in:
Sebastian Ullrich 2023-06-27 15:14:22 +01:00 • committed by Leonardo de Moura
parent 3104c223d8
commit e84a5891f8
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
doc/quickstart.md
View file

@ -21,6 +21,8 @@ See quick [walkthrough demo video](https://www.youtube.com/watch?v=yZo6k48L0VY).
info: latest update on nightly, lean version nightly-2021-12-05
info: downloading component 'lean'
```
If there is no popup, you probably have Elan installed already.
You may want to make sure that your default toolchain is Lean 4 in this case by running `elan default leanprover/lean4:nightly` and reopen the file, as the next step will fail otherwise.
1. While it is installing, you can paste the following Lean program into the new file: