Source code for https://apurvanakade.github.io/courses/lean_at_MC2020/index.html
Download this project using leanproject get apurvnakade/mc2020-Lean
To generate the html pages, you'll need pip and leanproject.
Run make html examples in the src folder.