In the Winter of 2026 I taught a course covering type theory and proof assistants in Lean. To make it easy on myself, I wrote all the course notes in Lean and used a code to slides converter I wrote called slider, which looks for markdown and a few different comment embedded tags to split the source into slides. The result is a set of easy to use and edit slides decks, which can be viewed here.
klavins/LeanW26
Folders and files
| Name | Name | Last commit date | ||
|---|---|---|---|---|