Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

feat(README) Point users to the tutorial project [ci skip] #1728

Merged
merged 3 commits into from Nov 22, 2019
Merged

feat(README) Point users to the tutorial project [ci skip] #1728

merged 3 commits into from Nov 22, 2019

Commits on Nov 22, 2019

  1. feat(README) Point users to the tutorial project 

    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.
    @kbuzzard
    kbuzzard committed Nov 22, 2019
    Configuration menu
    Copy the full SHA
    67cbf6e View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into kbuzzard-patch-2

    @bryangingechen
    bryangingechen committed Nov 22, 2019
    Configuration menu
    Copy the full SHA
    5ce7d01 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'master' into kbuzzard-patch-2

    @mergify
    mergify[bot] committed Nov 22, 2019
    Configuration menu
    Copy the full SHA
    ec7686d View commit details
    Browse the repository at this point in the history