Rename `Exercises` to `Bookshelf`.

Bookshelf.lean

@@ -0,0 +1,4 @@
+import Bookshelf.Apostol
+import Bookshelf.Avigad
+import Bookshelf.Enderton
+import Bookshelf.Fraleigh

Bookshelf/Apostol.lean

@@ -0,0 +1,2 @@
+import Bookshelf.Apostol.Chapter_I_03
+import Bookshelf.Apostol.Chapter_1_11

Bookshelf/Apostol/Chapter_1_11.lean

@@ -2,9 +2,9 @@ import Mathlib.Data.Real.Basic
 
 import Common.Real.Int
 
-/-! # Exercises.Apostol.Exercises_1_11 -/
+/-! # Apostol.Chapter_1_11 -/
 
-namespace Exercises.Apostol.Exercises_1_11
+namespace Apostol.Chapter_1_11
 
 /-! ## Exercise 4
 
@@ -73,4 +73,4 @@ Exercises 4(a) and (b) to the bracket on the right.
 -/
 theorem exercise_7b : True := sorry
 
-end Exercises.Apostol.Exercises_1_11
+end Apostol.Chapter_1_11

Bookshelf/Apostol/Chapter_1_11.tex

@@ -5,9 +5,9 @@
 \input{../../preamble}
 
 \newcommand{\link}[1]{\lean{../..}
-  {Exercises/Apostol/Exercises\_1\_11}
+  {Bookshelf/Apostol/Chapter\_1\_11}
-  {Exercises.Apostol.Exercises\_1\_11.#1}
+  {Apostol.Chapter\_1\_11.#1}
-  {Exercises\_1\_11.#1}
+  {Chapter\_1\_11.#1}
 }
 
 \begin{document}

Bookshelf/Apostol/Chapter_I_03.lean

@@ -1,11 +1,11 @@
 import Common.Real.Set
 
-/-! # Exercises.Apostol.Chapter_I_3
+/-! # Apostol.Chapter_I_3
 
 A Set of Axioms for the Real-Number System
 -/
 
-namespace Exercises.Apostol.Chapter_I_3
+namespace Apostol.Chapter_I_3
 
 #check Archimedean
 #check Real.exists_isLUB
@@ -640,4 +640,4 @@ the Archimedean property does not imply the least-upper-bound axiom.
 ###### TODO
 -/
 
-end Exercises.Apostol.Chapter_I_3
+end Apostol.Chapter_I_3

Bookshelf/Avigad.lean

@@ -0,0 +1,6 @@
+import Bookshelf.Avigad.Chapter2
+import Bookshelf.Avigad.Chapter3
+import Bookshelf.Avigad.Chapter4
+import Bookshelf.Avigad.Chapter5
+import Bookshelf.Avigad.Chapter7
+import Bookshelf.Avigad.Chapter8

Bookshelf/Avigad/Chapter2.lean

@@ -1,4 +1,4 @@
-/-! # Exercises.Avigad.Chapter2
+/-! # Avigad.Chapter2
 
 Dependent Type Theory
 -/
@@ -8,7 +8,7 @@ Dependent Type Theory
 Define the function `Do_Twice`, as described in Section 2.4.
 -/
 
-namespace Exercises.Avigad.Chapter2
+namespace Avigad.Chapter2
 
 namespace ex1
 
@@ -106,4 +106,4 @@ variable (d : ex3.vec Prop 3)
 
 end ex4
 
-end Exercises.Avigad.Chapter2
+end Avigad.Chapter2

Bookshelf/Avigad/Chapter3.lean

@@ -1,4 +1,4 @@
-/-! # Exercises.Avigad.Chapter3
+/-! # Avigad.Chapter3
 
 Propositions and Proofs
 -/
@@ -8,7 +8,7 @@ Propositions and Proofs
 Prove the following identities.
 -/
 
-namespace Exercises.Avigad.Chapter3
+namespace Avigad.Chapter3
 
 namespace ex1
 
@@ -164,4 +164,4 @@ theorem iff_not_self (hp : p) : ¬(p ↔ ¬p) :=
 
 end ex3
 
-end Exercises.Avigad.Chapter3
+end Avigad.Chapter3

Bookshelf/Avigad/Chapter4.lean

@@ -1,4 +1,4 @@
-/-! # Exercises.Avigad.Chapter4
+/-! # Avigad.Chapter4
 
 Quantifiers and Equality
 -/
@@ -9,7 +9,7 @@ Prove these equivalences. You should also try to understand why the reverse
 implication is not derivable in the last example.
 -/
 
-namespace Exercises.Avigad.Chapter4
+namespace Avigad.Chapter4
 
 namespace ex1
 
@@ -258,4 +258,4 @@ theorem log_mul {x y : Float} (hx : x > 0) (hy : y > 0) :
 
 end ex6
 
-end Exercises.Avigad.Chapter4
+end Avigad.Chapter4

Bookshelf/Avigad/Chapter5.lean

@@ -1,4 +1,4 @@
-/-! # Exercises.Avigad.Chapter5
+/-! # Avigad.Chapter5
 
 Tactics
 -/
@@ -9,7 +9,7 @@ Go back to the exercises in Chapter 3 and Chapter 4 and redo as many as you can
 now with tactic proofs, using also `rw` and `simp` as appropriate.
 -/
 
-namespace Exercises.Avigad.Chapter5
+namespace Avigad.Chapter5
 
 namespace ex1
 
@@ -461,4 +461,4 @@ theorem or_and_or_and_or (p q r : Prop) (hp : p)
 
 end ex2
 
-end Exercises.Avigad.Chapter5
+end Avigad.Chapter5

Bookshelf/Avigad/Chapter7.lean

@@ -1,9 +1,9 @@
-/-! # Exercises.Avigad.Chapter7
+/-! # Avigad.Chapter7
 
 Inductive Types
 -/
 
-namespace Exercises.Avigad.Chapter7
+namespace Avigad.Chapter7
 
 /-! #### Exercise 1
 
@@ -217,4 +217,4 @@ def eval_foo : Foo → List Nat → Nat
 
 end ex3
 
-end Exercises.Avigad.Chapter7
+end Avigad.Chapter7

Bookshelf/Avigad/Chapter8.lean

@@ -1,9 +1,9 @@
-/-! # Exercises.Avigad.Chapter8
+/-! # Avigad.Chapter8
 
 Induction and Recursion
 -/
 
-namespace Exercises.Avigad.Chapter8
+namespace Avigad.Chapter8
 
 /-! #### Exercise 1
 
@@ -206,4 +206,4 @@ theorem fuse_eq (v : Nat → Nat)
 
 end ex5
 
-end Exercises.Avigad.Chapter8
+end Avigad.Chapter8

Bookshelf/Enderton.lean

@@ -0,0 +1 @@
+import Bookshelf.Enderton.Chapter0

Bookshelf/Enderton/Chapter0.lean

@@ -1,11 +1,11 @@
 import Common.LTuple.Basic
 
-/-! # Exercises.Enderton.Chapter0
+/-! # Enderton.Chapter0
 
 Useful Facts About Sets
 -/
 
-namespace Exercises.Enderton.Chapter0
+namespace Enderton.Chapter0
 
 /--
 The following describes a so-called "generic" tuple. Like an `LTuple`, a generic
@@ -275,4 +275,4 @@ theorem lemma_0a (xs : GTuple α (n, m - 1)) (ys : LTuple α (m + k))
 
 end
 
-end Exercises.Enderton.Chapter0
+end Enderton.Chapter0

Bookshelf/Enderton/Chapter0.tex

@@ -3,8 +3,8 @@
 \input{../../preamble}
 
 \newcommand{\link}[1]{\lean{../..}
-  {Exercises/Enderton/Chapter0}
+  {Bookshelf/Enderton/Chapter0}
-  {Exercises.Enderton.Chapter0.#1}
+  {Enderton.Chapter0.#1}
   {Chapter0.#1}
 }
 

Bookshelf/Fraleigh.lean

@@ -0,0 +1 @@
+import Bookshelf.Fraleigh.Chapter1

Bookshelf/Fraleigh/Chapter1.lean

@@ -1,11 +1,11 @@
 import Mathlib.Data.Complex.Basic
 
-/-! # Exercises.Fraleign.Chapter1
+/-! # Fraleign.Chapter1
 
 Introduction and Examples
 -/
 
-namespace Exercises.Fraleign.Chapter1
+namespace Fraleign.Chapter1
 
 open Complex
 open HPow
@@ -21,4 +21,4 @@ theorem exercise1 : I^3 = 0 + (-1) * I := calc
     = I * (I * hPow I 1) := rfl
   _ = 0 + (-1) * I := by simp
 
-end Exercises.Fraleign.Chapter1
+end Fraleign.Chapter1

Exercises.lean

@@ -1,4 +0,0 @@
-import Exercises.Apostol
-import Exercises.Avigad
-import Exercises.Enderton
-import Exercises.Fraleigh

Exercises/Apostol.lean

@@ -1,2 +0,0 @@
-import Exercises.Apostol.Chapter_I_03
-import Exercises.Apostol.Chapter_1_11

Exercises/Avigad.lean

@@ -1,6 +0,0 @@
-import Exercises.Avigad.Chapter2
-import Exercises.Avigad.Chapter3
-import Exercises.Avigad.Chapter4
-import Exercises.Avigad.Chapter5
-import Exercises.Avigad.Chapter7
-import Exercises.Avigad.Chapter8

Exercises/Enderton.lean

@@ -1 +0,0 @@
-import Exercises.Enderton.Chapter0

Exercises/Fraleigh.lean

@@ -1 +0,0 @@
-import Exercises.Fraleigh.Chapter1

lakefile.lean

@@ -16,7 +16,7 @@ require «doc-gen4» from git
 
 @[default_target]
 lean_lib «Bookshelf» {
-  roots := #[`Common, `Exercises]
+  roots := #[`Bookshelf, `Common]
 }
 
 /--