From d54ecc43731b8d35001cae0a2fd29d8ce9c810fa Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 27 Jun 2023 15:16:21 +0100 Subject: [PATCH] doc: refer to mathlib4 instructions in quickstart --- doc/quickstart.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/doc/quickstart.md b/doc/quickstart.md index f7f0e000ea..0665b02a01 100644 --- a/doc/quickstart.md +++ b/doc/quickstart.md @@ -39,6 +39,8 @@ 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.* + 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.