From e84a5891f8879efbae3dd5d6fdb31c11483b7720 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 27 Jun 2023 15:14:22 +0100 Subject: [PATCH] doc: quickstart note on moving from Lean 3 to 4 --- doc/quickstart.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/doc/quickstart.md b/doc/quickstart.md index 4c5dd396c1..f7f0e000ea 100644 --- a/doc/quickstart.md +++ b/doc/quickstart.md @@ -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: