From e869d6f2d30becc92030e73ef13aad114c6c4806 Mon Sep 17 00:00:00 2001
From: Joshua Potter <jrpotter2112@gmail.com>
Date: Thu, 29 Jun 2023 15:30:48 -0600
Subject: [PATCH] Move aviary into Smullyan directory.

---
 Bookshelf.lean                                        | 4 ++--
 Bookshelf/Enderton.lean                               | 2 ++
 Bookshelf/Enderton/Set/Chapter_1.lean                 | 2 +-
 Bookshelf/Enderton/Set/Chapter_2.lean                 | 2 +-
 Bookshelf/Enderton/Set/Chapter_3.lean                 | 2 +-
 Bookshelf/Enderton/Set/OrderedPair.lean               | 2 +-
 Bookshelf/Enderton/Set/Relation.lean                  | 2 +-
 Bookshelf/Smullyan.lean                               | 1 +
 {Common/Combinator => Bookshelf/Smullyan}/Aviary.lean | 6 +-----
 Common.lean                                           | 1 -
 Common/Combinator.lean                                | 1 -
 11 files changed, 11 insertions(+), 14 deletions(-)
 create mode 100644 Bookshelf/Enderton.lean
 create mode 100644 Bookshelf/Smullyan.lean
 rename {Common/Combinator => Bookshelf/Smullyan}/Aviary.lean (95%)
 delete mode 100644 Common/Combinator.lean

diff --git a/Bookshelf.lean b/Bookshelf.lean
index 60405a2..0c2d8eb 100644
--- a/Bookshelf.lean
+++ b/Bookshelf.lean
@@ -1,5 +1,5 @@
 import Bookshelf.Apostol
 import Bookshelf.Avigad
-import Bookshelf.Enderton.Logic
-import Bookshelf.Enderton.Set
+import Bookshelf.Enderton
 import Bookshelf.Fraleigh
+import Bookshelf.Smullyan
diff --git a/Bookshelf/Enderton.lean b/Bookshelf/Enderton.lean
new file mode 100644
index 0000000..82b16ce
--- /dev/null
+++ b/Bookshelf/Enderton.lean
@@ -0,0 +1,2 @@
+import Bookshelf.Enderton.Logic
+import Bookshelf.Enderton.Set
\ No newline at end of file
diff --git a/Bookshelf/Enderton/Set/Chapter_1.lean b/Bookshelf/Enderton/Set/Chapter_1.lean
index e586f4e..2d380ee 100644
--- a/Bookshelf/Enderton/Set/Chapter_1.lean
+++ b/Bookshelf/Enderton/Set/Chapter_1.lean
@@ -1,6 +1,6 @@
 import Mathlib.Data.Set.Basic
 
-/-! # Enderton.Chapter_1
+/-! # Enderton.Set.Chapter_1
 
 Introduction
 -/
diff --git a/Bookshelf/Enderton/Set/Chapter_2.lean b/Bookshelf/Enderton/Set/Chapter_2.lean
index 4e32725..d107aba 100644
--- a/Bookshelf/Enderton/Set/Chapter_2.lean
+++ b/Bookshelf/Enderton/Set/Chapter_2.lean
@@ -2,7 +2,7 @@ import Bookshelf.Enderton.Set.Chapter_1
 import Common.Set.Basic
 import Mathlib.Data.Set.Lattice
 
-/-! # Enderton.Chapter_2
+/-! # Enderton.Set.Chapter_2
 
 Axioms and Operations
 -/
diff --git a/Bookshelf/Enderton/Set/Chapter_3.lean b/Bookshelf/Enderton/Set/Chapter_3.lean
index 8e753d0..7594056 100644
--- a/Bookshelf/Enderton/Set/Chapter_3.lean
+++ b/Bookshelf/Enderton/Set/Chapter_3.lean
@@ -2,7 +2,7 @@ import Bookshelf.Enderton.Set.Chapter_2
 import Bookshelf.Enderton.Set.OrderedPair
 import Bookshelf.Enderton.Set.Relation
 
-/-! # Enderton.Chapter_3
+/-! # Enderton.Set.Chapter_3
 
 Relations and Functions
 -/
diff --git a/Bookshelf/Enderton/Set/OrderedPair.lean b/Bookshelf/Enderton/Set/OrderedPair.lean
index f7236e2..35d094f 100644
--- a/Bookshelf/Enderton/Set/OrderedPair.lean
+++ b/Bookshelf/Enderton/Set/OrderedPair.lean
@@ -1,6 +1,6 @@
 import Common.Set.Basic
 
-/-! # Ordered Pairs
+/-! # Enderton.Set.OrderedPair
 
 A representation of an ordered pair in basic set theory. Like `Set`, it is
 assumed an ordered pair is homogeneous.
diff --git a/Bookshelf/Enderton/Set/Relation.lean b/Bookshelf/Enderton/Set/Relation.lean
index 1ed02d2..79294f7 100644
--- a/Bookshelf/Enderton/Set/Relation.lean
+++ b/Bookshelf/Enderton/Set/Relation.lean
@@ -1,6 +1,6 @@
 import Bookshelf.Enderton.Set.OrderedPair
 
-/-! # Relations
+/-! # Enderton.Set.Relation
 
 A representation of a relation, i.e. a set of ordered pairs. Like `Set`, it is
 assumed a relation is homogeneous.
diff --git a/Bookshelf/Smullyan.lean b/Bookshelf/Smullyan.lean
new file mode 100644
index 0000000..519684e
--- /dev/null
+++ b/Bookshelf/Smullyan.lean
@@ -0,0 +1 @@
+import Bookshelf.Smullyan.Aviary
\ No newline at end of file
diff --git a/Common/Combinator/Aviary.lean b/Bookshelf/Smullyan/Aviary.lean
similarity index 95%
rename from Common/Combinator/Aviary.lean
rename to Bookshelf/Smullyan/Aviary.lean
index 203592e..457a202 100644
--- a/Common/Combinator/Aviary.lean
+++ b/Bookshelf/Smullyan/Aviary.lean
@@ -1,4 +1,4 @@
-/-! # Common.Combinator.Aviary
+/-! # Smullyan.Aviary
 
 A collection of combinator birds representable in Lean. Certain duplicators,
 e.g. mockingbirds, are not directly expressible since they would require
@@ -7,10 +7,6 @@ encoding a signature in which an argument has types `α` *and* `α → α`.
 Duplicators that are included, e.g. the warbler, are not exactly correct
 considering they still have the same limitation described above during actual
 use. Their inclusion here serves more as pseudo-documentation than anything.
-
-[^1]: Smullyan, Raymond M. To Mock a Mockingbird: And Other Logic Puzzles
-      Including an Amazing Adventure in Combinatory Logic. Oxford: Oxford
-      university press, 2000.
 -/
 
 /-- #### Bald Eagle
diff --git a/Common.lean b/Common.lean
index 2d5b4b8..dc64440 100644
--- a/Common.lean
+++ b/Common.lean
@@ -1,4 +1,3 @@
-import Common.Combinator
 import Common.Finset
 import Common.List
 import Common.Logic
diff --git a/Common/Combinator.lean b/Common/Combinator.lean
deleted file mode 100644
index 1ff30b1..0000000
--- a/Common/Combinator.lean
+++ /dev/null
@@ -1 +0,0 @@
-import Common.Combinator.Aviary
\ No newline at end of file