use lake

leanprover-community · Nov 11, 2023 · fa9ae62 · fa9ae62
1 parent 5784576
commit fa9ae62
Showing 1 changed file with 5 additions and 2 deletions.
diff --git a/README.md b/README.md
@@ -20,8 +20,11 @@ to install Lean and a supporting toolchain.
 After that, download and open a copy of the repository
 by executing the following command in a terminal:
 ```
-leanproject get flt-regular
-code flt-regular
+git clone https://github.com/leanprover-community/flt-regular.git
+cd flt-regular
+lake exe cache get
+lake build
+code .
 ```
 For detailed instructions on how to work with Lean projects,
 see [this](https://leanprover-community.github.io/install/project.html).