Storing all of the content from the Learning Lean Seminar from Spring 2022
If you have the whole Lean toolchain up and running https://leanprover-community.github.io/get_started.html then the best way of getting everything off this repo is by running
leanproject get mpenciak/Lean-Seminar-Sp2022.git
If you don't have it all working, then simply running
git pull https://github.com/mpenciak/Lean-Seminar-Sp2022.git
will do the trick, but none of the demos will work because the dependencies will be unable to resolve. Eventually once you get Lean up and running on your personal computer you'll have to run
leanproject pull
to get all of the mathlib files.
It is also recommended that any exercise files you work on should be saved in a separate completed_exercises directory to avoid any erasing that may happen with merging from git.
If none of this makes sense yet, that's ok! We'll talk about it soon in the seminar soon!