Skip to main content

Questions tagged [lean-community]

The GitHub account `leanprover-community` which holds `mathlib`. This should not be confused with the GitHub account `leanprover` which holds the Lean source code.

1 question with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
0 votes
0 answers
23 views

How does one create a lean project even if it already exists e.g., lake +leanprover/lean4:nightly-2023-02-04 new my_project math?

I want to initialize a lean project but the folder I have already exists. How do I do this? e.g., ...
Charlie Parker's user avatar