From 973b76a6e2f0d64a9024b8ab369aef0065bf12d0 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 22 Mar 2022 16:35:14 -0700
Subject: [PATCH] doc: add `Examples` section

---
 doc/SUMMARY.md  | 2 ++
 doc/examples.md | 4 ++++
 2 files changed, 6 insertions(+)
 create mode 100644 doc/examples.md

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)