From 265803f7ac5b7b73f300352349e3fa2066330c4e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 22 Mar 2022 16:52:08 -0700
Subject: [PATCH] doc: fix links

---
 doc/SUMMARY.md | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/doc/SUMMARY.md b/doc/SUMMARY.md
index 75f2fface4..a64d271bec 100644
--- a/doc/SUMMARY.md
+++ b/doc/SUMMARY.md
@@ -4,10 +4,8 @@
 - [Tour of Lean](./tour.md)
 - [Setting Up Lean](./setup.md)
   - [Quickstart](./quickstart.md)
-
-# [Theorem Proving in Lean](./tpil.md)
-
-# [Examples](./examples.md)
+- [Theorem Proving in Lean](./tpil.md)
+- [Examples](./examples.md)
 
 # Language Manual
 <!-- - [Using Lean](./using_lean.md) -->