From 2e9adf0e04056270609cdeb986d917de143de342 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 22 Mar 2022 15:52:13 -0700
Subject: [PATCH] chore: remove broken documentation

---
 doc/SUMMARY.md   | 24 +++++++++++++-----------
 doc/inductive.md |  2 +-
 2 files changed, 14 insertions(+), 12 deletions(-)

diff --git a/doc/SUMMARY.md b/doc/SUMMARY.md
index e7fac63b11..74035c5764 100644
--- a/doc/SUMMARY.md
+++ b/doc/SUMMARY.md
@@ -5,23 +5,25 @@
 - [Setting Up Lean](./setup.md)
   - [Quickstart](./quickstart.md)
 
+# [Theorem Proving in Lean](https://leanprover.github.io/theorem_proving_in_lean4/title_page.html)
+
 # Language Manual
-- [Using Lean](./using_lean.md)
-- [Lexical Structure](./lexical_structure.md)
-- [Expressions](./expressions.md)
-- [Declarations](./declarations.md)
+<!-- - [Using Lean](./using_lean.md) -->
+<!-- - [Lexical Structure](./lexical_structure.md) -->
+<!-- - [Expressions](./expressions.md) -->
+<!-- - [Declarations](./declarations.md) -->
 - [Organizational features](./organization.md)
   - [Sections](./sections.md)
   - [Namespaces](./namespaces.md)
   - [Implicit Arguments](./implicit.md)
   - [Auto Bound Implicit Arguments](./autobound.md)
-- [Dependent Types](./deptypes.md)
-  - [Simple Type Theory](./simptypes.md)
-  - [Types as objects](./typeobjs.md)
-  - [Function Abstraction and Evaluation](./funabst.md)
-  - [Introducing Definitions](./introdef.md)
-  - [What makes dependent type theory dependent?](./dep.md)
-- [Tactics](./tactics.md)
+<!-- - [Dependent Types](./deptypes.md) -->
+<!--   - [Simple Type Theory](./simptypes.md) -->
+<!--   - [Types as objects](./typeobjs.md) -->
+<!--   - [Function Abstraction and Evaluation](./funabst.md) -->
+<!--   - [Introducing Definitions](./introdef.md) -->
+<!--   - [What makes dependent type theory dependent?](./dep.md) -->
+<!-- - [Tactics](./tactics.md) -->
 - [Syntax Extensions](./syntax.md)
   - [The `do` Notation](./do.md)
   - [User-defined notation](./notation.md)
diff --git a/doc/inductive.md b/doc/inductive.md
index 487748ae57..f93a81fc00 100644
--- a/doc/inductive.md
+++ b/doc/inductive.md
@@ -1,3 +1,3 @@
 # Inductive Types
 
-TODO
\ No newline at end of file
+[Theorem Proving in Lean](https://leanprover.github.io/theorem_proving_in_lean4/inductive_types.html) has a chapter about inductive datatypes.