Examples ======== - [A Certified Type Checker](examples/tc.lean.html) - [The Well-Typed Interpreter](examples/interp.lean.html) - [Dependent de Bruijn Indices](examples/deBruijn.lean.html) - [Parametric Higher-Order Abstract Syntax](examples/phoas.lean.html)