Learn Lean 4

Chapters

• 0 Setup
• 1 Values and Functions
• 2 Pattern matching and inductive types
• 3 Structures and type classes
• 4 Lists
• 5 Arrays
• 6 Strings (UTF-8, iterators)
• 7 `HashMap`, `HashSet`, `TreeMap`
• 8 `Option`, `Except`, and error handling
• 9 The `IO` monad and `do` notation
• 10 File I/O
• 11 Processes and pipes
• 12 Sockets and networking
• 13 Tasks, refs, and mutexes
• 14 JSON
• 15 Macros
• 16 Type-Level Programming (with comparisons to Haskell)
• 17 Coming from Haskell
• 18 Why Lean 4 runs like C, not GHC