| Examples | |
| ======== | |
| - [Palindromes](examples/palindromes.lean.md) | |
| - [Binary Search Trees](examples/bintree.lean.md) | |
| - [A Certified Type Checker](examples/tc.lean.md) | |
| - [The Well-Typed Interpreter](examples/interp.lean.md) | |
| - [Dependent de Bruijn Indices](examples/deBruijn.lean.md) | |
| - [Parametric Higher-Order Abstract Syntax](examples/phoas.lean.md) |