Functional programming patterns
The programming and abstraction material from the former Lean 4 course, rebuilt around compiler-checked exercises. Work with higher-order functions, records, exhaustive pattern matches, structural recursion on naturals and lists, termination, and instance synthesis.
Sign in to track your progress
- Functions as valuesPass behavior into a reusable higher-order function.10 min
- Structures and record updatesModel named fields and construct precise modified copies.11 min
- Exhaustive pattern matchingDefine behavior for every constructor and prove it by cases.12 min
- Recursion on natural numbersWrite base and successor cases that Lean can see decrease.12 min
- Recursion on listsFollow nil and cons while staying polymorphic in the elements.12 min
- Why recursion must terminateConnect decreasing arguments, total functions, and sound logic.10 min
- Classes and instancesDescribe shared behavior and let Lean synthesize an implementation.13 min