From e29795c55eba9c484c6459860cd6316538a8d498 Mon Sep 17 00:00:00 2001
From: Joshua Potter <jrpotter2112@gmail.com>
Date: Tue, 26 Sep 2023 09:55:04 -0600
Subject: [PATCH] Add links to different books.

---
 Bookshelf/Apostol.lean        | 16 +++++++++++++++-
 Bookshelf/Avigad.lean         | 16 +++++++++++++++-
 Bookshelf/Enderton/Logic.lean | 15 ++++++++++++++-
 Bookshelf/Enderton/Set.lean   | 19 ++++++++++++++++++-
 Bookshelf/Fraleigh.lean       |  9 +++++++++
 DocGen4/Output/Index.lean     |  9 +++++----
 6 files changed, 76 insertions(+), 8 deletions(-)

diff --git a/Bookshelf/Apostol.lean b/Bookshelf/Apostol.lean
index 1f245ca..0c9fc12 100644
--- a/Bookshelf/Apostol.lean
+++ b/Bookshelf/Apostol.lean
@@ -1,2 +1,16 @@
 import Bookshelf.Apostol.Chapter_I_03
-import Bookshelf.Apostol.Chapter_1_11
\ No newline at end of file
+import Bookshelf.Apostol.Chapter_1_11
+
+/-! # Calculus, Vol. 1: One-Variable Calculus, with an Introduction to Linear Algebra
+
+## Apostol, Tom M.
+
+### LaTeX
+
+Full set of [proofs and exercises](Bookshelf/Apostol.pdf).
+
+### Lean
+
+* [Chapter I.03: A Set of Axioms for the Real-Number System](Bookshelf/Apostol/Chapter_I_03.html)
+* [Chapter 1.11: Exercises](Bookshelf/Apostol/Chapter_1_11.html)
+-/
\ No newline at end of file
diff --git a/Bookshelf/Avigad.lean b/Bookshelf/Avigad.lean
index ab51323..bc83c0f 100644
--- a/Bookshelf/Avigad.lean
+++ b/Bookshelf/Avigad.lean
@@ -3,4 +3,18 @@ import Bookshelf.Avigad.Chapter_3
 import Bookshelf.Avigad.Chapter_4
 import Bookshelf.Avigad.Chapter_5
 import Bookshelf.Avigad.Chapter_7
-import Bookshelf.Avigad.Chapter_8
\ No newline at end of file
+import Bookshelf.Avigad.Chapter_8
+
+/-! # Theorem Proving in Lean
+
+## Avigad, Jeremy.
+
+### Lean
+
+* [Chapter 2: Dependent Type Theory](Bookshelf/Avigad/Chapter_2.html)
+* [Chapter 3: Propositions and Proofs](Bookshelf/Avigad/Chapter_3.html)
+* [Chapter 4: Quantifiers and Equality](Bookshelf/Avigad/Chapter_4.html)
+* [Chapter 5: Tactics](Bookshelf/Avigad/Chapter_5.html)
+* [Chapter 7: Inductive Types](Bookshelf/Avigad/Chapter_7.html)
+* [Chapter 8: Induction and Recursion](Bookshelf/Avigad/Chapter_8.html)
+-/
\ No newline at end of file
diff --git a/Bookshelf/Enderton/Logic.lean b/Bookshelf/Enderton/Logic.lean
index 3edb997..5b7d7aa 100644
--- a/Bookshelf/Enderton/Logic.lean
+++ b/Bookshelf/Enderton/Logic.lean
@@ -1 +1,14 @@
-import Bookshelf.Enderton.Logic.Chapter_1
\ No newline at end of file
+import Bookshelf.Enderton.Logic.Chapter_1
+
+/-! # A Mathematical Introduction to Logic
+
+## Enderton, Herbert B.
+
+### LaTeX
+
+Full set of [proofs and exercises](Bookshelf/Enderton/Logic.pdf).
+
+### Lean
+
+* [Chapter 1: Sentential Logic](Bookshelf/Enderton/Logic/Chapter_1.html)
+-/
\ No newline at end of file
diff --git a/Bookshelf/Enderton/Set.lean b/Bookshelf/Enderton/Set.lean
index 0aaae73..2c8e963 100644
--- a/Bookshelf/Enderton/Set.lean
+++ b/Bookshelf/Enderton/Set.lean
@@ -4,4 +4,21 @@ import Bookshelf.Enderton.Set.Chapter_3
 import Bookshelf.Enderton.Set.Chapter_4
 import Bookshelf.Enderton.Set.Chapter_6
 import Bookshelf.Enderton.Set.OrderedPair
-import Bookshelf.Enderton.Set.Relation
\ No newline at end of file
+import Bookshelf.Enderton.Set.Relation
+
+/-! # Elements of Set Theory
+
+## Enderton, Herbert B.
+
+### LaTeX
+
+Full set of [proofs and exercises](Bookshelf/Enderton/Set.pdf).
+
+### Lean
+
+* [Chapter 1: Introduction](Bookshelf/Enderton/Set/Chapter_1.html)
+* [Chapter 2: Axioms and Operations](Bookshelf/Enderton/Set/Chapter_2.html)
+* [Chapter 3: Relations and Functions](Bookshelf/Enderton/Set/Chapter_3.html)
+* [Chapter 4: Natural Numbers](Bookshelf/Enderton/Set/Chapter_4.html)
+* [Chapter 6: Cardinal Numbers and the Axiom of Choice](Bookshelf/Enderton/Set/Chapter_6.html)
+-/
\ No newline at end of file
diff --git a/Bookshelf/Fraleigh.lean b/Bookshelf/Fraleigh.lean
index b03ab15..499d4fb 100644
--- a/Bookshelf/Fraleigh.lean
+++ b/Bookshelf/Fraleigh.lean
@@ -1 +1,10 @@
 import Bookshelf.Fraleigh.Chapter_1
+
+/-! # A First Course in Abstract Algebra
+
+## Fraleigh, John B.
+
+### Lean
+
+* [Chapter 1: Introduction and Examples](Bookshelf/Fraleigh/Chapter_1.html)
+-/
\ No newline at end of file
diff --git a/DocGen4/Output/Index.lean b/DocGen4/Output/Index.lean
index c042e40..f12b0fa 100644
--- a/DocGen4/Output/Index.lean
+++ b/DocGen4/Output/Index.lean
@@ -24,14 +24,15 @@ def index : BaseHtmlM Html := do templateExtends (baseHtml "Index") <|
 
       <h2>In Progress</h2>
       <ul>
-        <li>Apostol, Tom M. Calculus, Vol. 1: One-Variable Calculus, with an Introduction to Linear Algebra. 2nd ed. Vol. 1. 2 vols. Wiley, 1991.</li>
-        <li>Enderton, Herbert B. A Mathematical Introduction to Logic. 2nd ed. San Diego: Harcourt/Academic Press, 2001.</li>
-        <li>Enderton, Herbert B. Elements of Set Theory. New York: Academic Press, 1977.</li>
+        <li><a href={s!"{← getRoot}Bookshelf/Apostol.html"}>Apostol, Tom M. Calculus, Vol. 1: One-Variable Calculus, with an Introduction to Linear Algebra. 2nd ed. Vol. 1. 2 vols. Wiley, 1991.</a></li>
+        <li><a href={s!"{← getRoot}Bookshelf/Enderton/Logic.html"}>Enderton, Herbert B. A Mathematical Introduction to Logic. 2nd ed. San Diego: Harcourt/Academic Press, 2001.</a></li>
+        <li><a href={s!"{← getRoot}Bookshelf/Enderton/Set.html"}>Enderton, Herbert B. Elements of Set Theory. New York: Academic Press, 1977.</a></li>
+        <li><a href={s!"{← getRoot}Bookshelf/Fraleigh.html"}>Fraleigh, John B. A First Course in Abstract Algebra, n.d.</a></li>
       </ul>
 
       <h2>Complete</h2>
       <ul>
-        <li>Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d.</li>
+        <li><a href={s!"{← getRoot}Bookshelf/Avigad.html"}>Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d.</a></li>
       </ul>
 
       <h2>Pending</h2>