Functional programming
Write polymorphic higher-order functions, records, exhaustive matches, recursive programs on numbers and lists, your own list map with a length proof, terminating functions, and code that uses type classes.
Progress is kept in this browser until you sign in
- Functions as valuesPass behaviour as an argument, then prove a law about every input.10 min
- Functions you build as you goCapture local context in a lambda, and return a function as a result.11 min
- Structures and record updatesNamed fields, precise copies, and why eta closes a round trip.11 min
- Define your own structureFields, the constructor Lean generates for you, and record updates.12 min
- Exhaustive pattern matchingWildcards, exhaustiveness, and covering every constructor in a proof.12 min
- Recursion on natural numbersBase and successor cases, and the equations they hand you for free.12 min
- Recursion on listsPeel constructors off a list while staying polymorphic in the elements.12 min
- Write and verify your own mapBuild a polymorphic higher-order list function, then prove that it preserves length.18 min
- Walk two lists at onceMatch two lists together and combine them element by element.13 min
- Why recursion must terminateWhat Lean rejects, why it must, and what totality buys your proofs.10 min
- Recursion that is not structuralRecursive calls on computed values, and the measure that proves they stop.14 min
- Classes and instancesDescribe shared behaviour and let Lean pick the implementation.13 min