| Examples | |
| ======== | |
| - [A Certified Type Checker](https://github.com/leanprover/lean4/blob/master/doc/examples/tc.lean) | |
| - [The Well-Typed Interpreter](https://github.com/leanprover/lean4/blob/master/doc/examples/interp.lean) | |
| - [Dependent de Bruijn Indices](https://github.com/leanprover/lean4/blob/master/doc/examples/deBruijn.lean) |