lean-iap

IAP 2026 class about Lean (mirror)

Commits at 707e1b738f00c21d1b5b04dfcf4a258a8caa7232

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