lean-iap

IAP 2026 class about Lean (mirror)

Commits at main

  1. 1befd72d Cancel the third office hours, minor tweaks for third lecture code Anthony Wang authored at Anthony Wang comitted at
  2. d98d5788 Minor random tweaks Anthony Wang authored at Anthony Wang comitted at
  3. 707e1b73 OK sure we can do mvcgen today probably Anthony Wang authored at Anthony Wang comitted at
  4. d627c935 Change reading recs too Anthony Wang authored at Anthony Wang comitted at
  5. 5715b3b4 Make lec title capitalization consistent Anthony Wang authored at Anthony Wang comitted at
  6. 304be42e More monad stuff yay Anthony Wang authored at Anthony Wang comitted at
  7. 25cb5db7 Don't need [Nonempty α] for cjq2 Anthony Wang authored at Anthony Wang comitted at
  8. 813d3b2e Welp won't get to advanced topics I guess Anthony Wang authored at Anthony Wang comitted at
  9. 90fc24de Move problems to Pset1.5.lean Anthony Wang authored at Anthony Wang comitted at
  10. be2c037a Finished lec 2 Anthony Wang authored at Anthony Wang comitted at
  11. 800a7ee2 Even more exercises yay Anthony Wang authored at Anthony Wang comitted at
  12. bb4d3e7f Link to Git repo on homepage Anthony Wang authored at Anthony Wang comitted at
  13. 75dcf438 Add a lot of exercises Anthony Wang authored at Anthony Wang comitted at
  14. e3d5d438 More example code for lec 2 Anthony Wang authored at Anthony Wang comitted at
  15. a9e13937 Add CC BY-SA license Anthony Wang authored at Anthony Wang comitted at
  16. 6be03a3d More random stuff Anthony Wang authored at Anthony Wang comitted at
  17. 894b9410 Actually move the video player thing down even more Anthony Wang authored at Anthony Wang comitted at
  18. 98ebeb1e Final tweaks for slides Anthony Wang authored at Anthony Wang comitted at
  19. 7e004a76 Mostly done with slides yay Anthony Wang authored at Anthony Wang comitted at
  20. a672485a Finished type theory notes finally Anthony Wang authored at Anthony Wang comitted at
  21. 9c041d5d Add more functor/applicative/monad problems to pset2, move some to pset3 Anthony Wang authored at Anthony Wang comitted at
  22. ff509108 More examples for lectures Anthony Wang authored at Anthony Wang comitted at
  23. 8d59b729 Move tactics mode problem from Pset2 to pset3, add Id monad problem Anthony Wang authored at Anthony Wang comitted at
  24. 5c0b8979 Add Lean primes example too Anthony Wang authored at Anthony Wang comitted at
  25. 4d748e8e Mostly done with Basic.lean Anthony Wang authored at Anthony Wang comitted at
  26. 801d2638 More random stuff for remaining files - Move universe example to Advanced.lean since it wouldn't work well as a pset problem - Fancy ∅ symbol - Some Olympiad problems for psets? Anthony Wang authored at Anthony Wang comitted at
  27. 89e027b6 Add another fun pset problem Anthony Wang authored at Anthony Wang comitted at
  28. d387e086 Add more resources and type theory blackboard plans Anthony Wang authored at Anthony Wang comitted at
  29. e8d51409 Make site slightly thinner Anthony Wang authored at Anthony Wang comitted at
  30. 54622194 Update office hours time Anthony Wang authored at Anthony Wang comitted at