lean-iap

IAP 2026 class about Lean (mirror)

  1. 1
  2. 2
  3. 3
  4. 4
  5. 5
  6. 6
  7. 7
  8. 8

import Cluedump
import GenerateSlidesLib

#leantex_config latexConfig

unsafe def main : IO Unit := do
   generateSlides latexConfig