Skip to main content
Proof Assistants Beta

Return to Answer

added 93 characters in body
Source Link
Alex Byard
Alex Byard
  • 486
  • 1
  • 13

Here's how I go about setting up a project. This information can be found in the Lean documentation. In a terminal go to the folder you want to create your project in. We'll call this project my_project. In your terminal run

lake +leanprover/lean4:nightly-2023-02-04 new my_project math

The date here doesn't need to be changed. The math keyword adds mathlib4 to the dependencies of the project so that you can import Mathlib in your project files.

Go inside the my_project folder and run lake update, then lake exe cache get, and then mkdir MyProject. Launch VS Code by writing code . and make sure you are in my_project. The .lean files for your project should go in the MyProject folder.

The documentation is here.

Here's how I go about setting up a project. This information can be found in the Lean documentation. In a terminal go to the folder you want to create your project in. We'll call this project my_project. In your terminal run

lake +leanprover/lean4:nightly-2023-02-04 new my_project math

The date here doesn't need to be changed. The math keyword adds mathlib4 to the dependencies of the project so that you can import Mathlib in your project files.

Go inside the my_project folder and run lake update, then lake exe cache get, and then mkdir MyProject. Launch VS Code by writing code . and make sure you are in my_project. The .lean files for your project should go in the MyProject folder.

Here's how I go about setting up a project. This information can be found in the Lean documentation. In a terminal go to the folder you want to create your project in. We'll call this project my_project. In your terminal run

lake +leanprover/lean4:nightly-2023-02-04 new my_project math

The date here doesn't need to be changed. The math keyword adds mathlib4 to the dependencies of the project so that you can import Mathlib in your project files.

Go inside the my_project folder and run lake update, then lake exe cache get, and then mkdir MyProject. Launch VS Code by writing code . and make sure you are in my_project. The .lean files for your project should go in the MyProject folder.

The documentation is here.

Source Link
Alex Byard
Alex Byard
  • 486
  • 1
  • 13

Here's how I go about setting up a project. This information can be found in the Lean documentation. In a terminal go to the folder you want to create your project in. We'll call this project my_project. In your terminal run

lake +leanprover/lean4:nightly-2023-02-04 new my_project math

The date here doesn't need to be changed. The math keyword adds mathlib4 to the dependencies of the project so that you can import Mathlib in your project files.

Go inside the my_project folder and run lake update, then lake exe cache get, and then mkdir MyProject. Launch VS Code by writing code . and make sure you are in my_project. The .lean files for your project should go in the MyProject folder.