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

doc: fix typo in quickstart.md

Browse source
This commit is contained in:
Sebastian Ullrich 2023-10-04 17:49:50 +02:00 • committed by GitHub
parent 89b65c8f1d
commit dceed634a0
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
doc/quickstart.md
View file

@ -39,7 +39,7 @@ You are set up!
## Create a Lean Project
*If your goal is to contribute to [mathlib4](https://github.com/leanprover-community/mathlib4) or use it as a depdency, please see its readme for specific instructions on how to do that.*
*If your goal is to contribute to [mathlib4](https://github.com/leanprover-community/mathlib4) or use it as a dependency, please see its readme for specific instructions on how to do that.*
You can now create a Lean project in a new folder. Run `lake init foo` from "View > Terminal" to create a package, followed by `lake build` to get an executable version of your Lean program.
On Linux/macOS, you first have to follow the instructions printed by the Lean installation or log out and in again for the Lean executables to be available in you terminal.