Skip to content

Commit

Permalink
feat(README) Point users to the tutorial project (leanprover-communit…
Browse files Browse the repository at this point in the history
…y#1728)

I think the tutorial project is a good place to start, and if other people don't think it is then I think they might want to consider adding more files to the tutorial project. I think mathlib is intimidating for beginners and this is a much better idea. However the link to the tutorial project is not even available on the main page -- you have to click through an installation procedure and find it at the bottom, and even then the first thing is suggests is that you make a new project, which I think is harder than getting the tutorial project up and running. This PR proposes that we point people directly to the tutorial project -- they will probably notice the existence of the tutorial project before they have even installed Lean/mathlib and will hence have it at the back of their mind once they've got things up and running.
  • Loading branch information
kbuzzard authored and anrddh committed May 15, 2020
1 parent 9018ad1 commit 9962819
Showing 1 changed file with 4 additions and 0 deletions.
4 changes: 4 additions & 0 deletions README.md
Expand Up @@ -17,6 +17,10 @@ You can find detailed instructions to install Lean, mathlib, and supporting tool
* On [MacOS](docs/install/macos.md)
* On [Windows](docs/install/windows.md)

## Experimenting

Got everything installed? Why not start with the [tutorial project](https://github.com/leanprover-community/mathlib/blob/master/docs/install/project.md#working-on-an-existing-package)?

## Documentation

Besides the installation guides above and [Lean's general
Expand Down

0 comments on commit 9962819

Please sign in to comment.