| # Summary | |
| - [What is Lean](./whatIsLean.md) | |
| - [Tour of Lean](./tour.md) | |
| - [Setting Up Lean](./quickstart.md) | |
| - [Extended Setup Notes](./setup.md) | |
| - [Theorem Proving in Lean](./tpil.md) | |
| - [Functional Programming in Lean](fplean.md) | |
| - [Examples](./examples.md) | |
| - [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) | |
| - [Syntax Examples](./syntax_examples.md) | |
| - [Balanced Parentheses](./syntax_example.md) | |
| - [Arithmetic DSL](./metaprogramming-arith.md) | |
| # Language Manual | |
| - [The Lean Reference Manual](./reference.md) | |
| # Other | |
| - [Frequently Asked Questions](./faq.md) | |
| - [Significant Changes from Lean 3](./lean3changes.md) | |
| - [Syntax Highlighting Lean in LaTeX](./syntax_highlight_in_latex.md) | |
| - [User Widgets](examples/widgets.lean.md) | |
| - [Semantic Highlighting](./semantic_highlighting.md) | |
| # Development | |
| - [Development Guide](./dev/index.md) | |
| - [Building Lean](./make/index.md) | |
| - [Ubuntu Setup](./make/ubuntu.md) | |
| - [macOS Setup](./make/osx-10.9.md) | |
| - [Windows MSYS2 Setup](./make/msys2.md) | |
| - [Windows with WSL](./make/wsl.md) | |
| - [Bootstrapping](./dev/bootstrap.md) | |
| - [Testing](./dev/testing.md) | |
| - [Debugging](./dev/debugging.md) | |
| - [Commit Convention](./dev/commit_convention.md) | |
| - [Release checklist](./dev/release_checklist.md) | |
| - [Building This Manual](./dev/mdbook.md) | |
| - [Foreign Function Interface](./dev/ffi.md) |