diff --git a/doc/SUMMARY.md b/doc/SUMMARY.md
index c32f57d0bf..88892f6a18 100644
--- a/doc/SUMMARY.md
+++ b/doc/SUMMARY.md
@@ -7,6 +7,8 @@
 
 # [Theorem Proving in Lean](https://leanprover.github.io/theorem_proving_in_lean4/title_page.html)
 
+# [Examples](./examples.md)
+
 # Language Manual
 <!-- - [Using Lean](./using_lean.md) -->
 <!-- - [Lexical Structure](./lexical_structure.md) -->
diff --git a/doc/examples.md b/doc/examples.md
new file mode 100644
index 0000000000..57d2214d00
--- /dev/null
+++ b/doc/examples.md
@@ -0,0 +1,4 @@
+Examples
+========
+
+- [The Well-Typed Interpreter](./doc/examples/interp.lean)