From 74cb289d48d0c17321d09d829431f384841fe78e Mon Sep 17 00:00:00 2001
From: Jeremy Avigad <avigad@cmu.edu>
Date: Tue, 16 Sep 2014 14:58:54 -0400
Subject: [PATCH] refactor(library): rename algebra directory to struc, move
 categories.lean to algebra

---
 library/{struc/struc.md => algebra/algebra.md} | 7 ++++---
 library/{struc => algebra}/binary.lean         | 0
 library/{data => algebra}/category.lean        | 2 +-
 library/{struc => algebra}/function.lean       | 0
 library/{struc => algebra}/relation.lean       | 2 +-
 library/{struc => algebra}/wf.lean             | 0
 library/data/int/basic.lean                    | 4 ++--
 library/data/nat/basic.lean                    | 2 +-
 library/data/nat/div.lean                      | 2 +-
 library/data/quotient/basic.lean               | 2 +-
 library/data/quotient/classical.lean           | 2 +-
 library/data/quotient/util.lean                | 2 +-
 library/hott/path.lean                         | 2 +-
 library/library.md                             | 2 +-
 library/logic/axioms/classical.lean            | 2 +-
 library/logic/axioms/funext.lean               | 7 ++++---
 library/logic/core/instances.lean              | 2 +-
 library/logic/logic.md                         | 4 +---
 tests/lean/run/cat.lean                        | 2 +-
 tests/lean/run/coe11.lean                      | 2 +-
 tests/lean/run/congr_imp_bug.lean              | 2 +-
 tests/lean/run/div2.lean                       | 2 +-
 tests/lean/run/elab_bug1.lean                  | 2 +-
 tests/lean/run/fun.lean                        | 2 +-
 tests/lean/run/rel.lean                        | 2 +-
 tests/lean/slow/nat_bug2.lean                  | 2 +-
 tests/lean/slow/nat_wo_hints.lean              | 2 +-
 27 files changed, 31 insertions(+), 31 deletions(-)
 rename library/{struc/struc.md => algebra/algebra.md} (68%)
 rename library/{struc => algebra}/binary.lean (100%)
 rename library/{data => algebra}/category.lean (99%)
 rename library/{struc => algebra}/function.lean (100%)
 rename library/{struc => algebra}/relation.lean (99%)
 rename library/{struc => algebra}/wf.lean (100%)

diff --git a/library/struc/struc.md b/library/algebra/algebra.md
similarity index 68%
rename from library/struc/struc.md
rename to library/algebra/algebra.md
index 63be3cc704..019e2d9528 100644
--- a/library/struc/struc.md
+++ b/library/algebra/algebra.md
@@ -1,9 +1,10 @@
-struc
-=====
+algebra
+=======
 
-Axiomatic properties and structures.
+Algebraic structures.
 
 * [function](function.lean)
 * [relation](relation.lean)
 * [binary](binary.lean) : binary operations
 * [wf](wf.lean) : well-founded relations
+* [category](category.lean)
\ No newline at end of file
diff --git a/library/struc/binary.lean b/library/algebra/binary.lean
similarity index 100%
rename from library/struc/binary.lean
rename to library/algebra/binary.lean
diff --git a/library/data/category.lean b/library/algebra/category.lean
similarity index 99%
rename from library/data/category.lean
rename to library/algebra/category.lean
index b5cfe84cc7..ff5f749b1b 100644
--- a/library/data/category.lean
+++ b/library/algebra/category.lean
@@ -5,7 +5,7 @@
 -- category
 import logic.core.eq logic.core.connectives
 import data.unit data.sigma data.prod
-import struc.function
+import algebra.function
 
 open eq
 
diff --git a/library/struc/function.lean b/library/algebra/function.lean
similarity index 100%
rename from library/struc/function.lean
rename to library/algebra/function.lean
diff --git a/library/struc/relation.lean b/library/algebra/relation.lean
similarity index 99%
rename from library/struc/relation.lean
rename to library/algebra/relation.lean
index 405579076d..5df8353656 100644
--- a/library/struc/relation.lean
+++ b/library/algebra/relation.lean
@@ -2,7 +2,7 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Jeremy Avigad
 
--- struc.relation
+-- algebra.relation
 -- ==============
 
 import logic.core.prop
diff --git a/library/struc/wf.lean b/library/algebra/wf.lean
similarity index 100%
rename from library/struc/wf.lean
rename to library/algebra/wf.lean
diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean
index 83e43b0346..a5383efde6 100644
--- a/library/data/int/basic.lean
+++ b/library/data/int/basic.lean
@@ -7,8 +7,8 @@
 
 -- The integers, with addition, multiplication, and subtraction.
 
-import ..nat.basic ..nat.order ..nat.sub ..prod ..quotient ..quotient tools.tactic struc.relation
-import struc.binary
+import ..nat.basic ..nat.order ..nat.sub ..prod ..quotient ..quotient tools.tactic algebra.relation
+import algebra.binary
 import tools.fake_simplifier
 
 open nat
diff --git a/library/data/nat/basic.lean b/library/data/nat/basic.lean
index a19bdd4dcc..c849b353a3 100644
--- a/library/data/nat/basic.lean
+++ b/library/data/nat/basic.lean
@@ -7,7 +7,7 @@
 --
 -- Basic operations on the natural numbers.
 
-import logic data.num tools.tactic struc.binary tools.helper_tactics
+import logic data.num tools.tactic algebra.binary tools.helper_tactics
 import logic.core.inhabited
 
 open tactic binary eq_ops
diff --git a/library/data/nat/div.lean b/library/data/nat/div.lean
index 9c6a32c089..78eb3a7b91 100644
--- a/library/data/nat/div.lean
+++ b/library/data/nat/div.lean
@@ -8,7 +8,7 @@
 -- This is a continuation of the development of the natural numbers, with a general way of
 -- defining recursive functions, and definitions of div, mod, and gcd.
 
-import logic .sub struc.relation data.prod
+import logic .sub algebra.relation data.prod
 import tools.fake_simplifier
 
 open nat relation relation.iff_ops prod
diff --git a/library/data/quotient/basic.lean b/library/data/quotient/basic.lean
index d16e3b4b8f..5f5568e9b0 100644
--- a/library/data/quotient/basic.lean
+++ b/library/data/quotient/basic.lean
@@ -5,7 +5,7 @@
 -- Theory data.quotient
 -- ====================
 
-import logic tools.tactic ..subtype logic.core.cast struc.relation data.prod
+import logic tools.tactic ..subtype logic.core.cast algebra.relation data.prod
 import logic.core.instances
 import .util
 
diff --git a/library/data/quotient/classical.lean b/library/data/quotient/classical.lean
index 0fb6873717..e8a61751e2 100644
--- a/library/data/quotient/classical.lean
+++ b/library/data/quotient/classical.lean
@@ -2,7 +2,7 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Floris van Doorn
 
-import struc.relation logic.core.nonempty data.subtype
+import algebra.relation logic.core.nonempty data.subtype
 import .basic
 import logic.axioms.classical logic.axioms.hilbert logic.axioms.funext
 
diff --git a/library/data/quotient/util.lean b/library/data/quotient/util.lean
index 9abb1697bb..886d372b76 100644
--- a/library/data/quotient/util.lean
+++ b/library/data/quotient/util.lean
@@ -2,7 +2,7 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Floris van Doorn
 
-import logic ..prod struc.relation
+import logic ..prod algebra.relation
 import tools.fake_simplifier
 
 open prod eq_ops
diff --git a/library/hott/path.lean b/library/hott/path.lean
index 7766c86d5f..b85123865b 100644
--- a/library/hott/path.lean
+++ b/library/hott/path.lean
@@ -8,7 +8,7 @@
 -- o Try doing these proofs with tactics.
 -- o Try using the simplifier on some of these proofs.
 
-import general_notation struc.function
+import general_notation algebra.function
 
 open function
 
diff --git a/library/library.md b/library/library.md
index 708c1c0360..2cb975a162 100644
--- a/library/library.md
+++ b/library/library.md
@@ -6,7 +6,7 @@ The Lean library is contained in the following modules and directories:
 * [general_notation](general_notation.lean) : commonly shared notation
 * [logic](logic/logic.md) : logical constructs and axioms
 * [data](data/data.md) : concrete datatypes and type constructors
-* [struc](struc/struc.md) : axiomatic structures
+* [algebra](algebra/algebra.md) : algebraic structures
 * [hott](hott/hott.md) : homotopy type theory
 * [tools](tools/tools.md) : additional tools
 
diff --git a/library/logic/axioms/classical.lean b/library/logic/axioms/classical.lean
index 60c9ab9b84..de437e6cdb 100644
--- a/library/logic/axioms/classical.lean
+++ b/library/logic/axioms/classical.lean
@@ -5,7 +5,7 @@
 -- logic.axioms.classical
 -- ======================
 
-import logic.core.quantifiers logic.core.cast struc.relation
+import logic.core.quantifiers logic.core.cast algebra.relation
 
 open eq_ops
 
diff --git a/library/logic/axioms/funext.lean b/library/logic/axioms/funext.lean
index 508e799b76..4920a9fc59 100644
--- a/library/logic/axioms/funext.lean
+++ b/library/logic/axioms/funext.lean
@@ -1,10 +1,11 @@
-----------------------------------------------------------------------------------------------------
 -- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura
-----------------------------------------------------------------------------------------------------
 
-import logic.core.eq struc.function
+-- logic.axioms.funext
+-- ===================
+
+import logic.core.eq algebra.function
 open function
 
 -- Function extensionality
diff --git a/library/logic/core/instances.lean b/library/logic/core/instances.lean
index 4267536f7c..0bfca00758 100644
--- a/library/logic/core/instances.lean
+++ b/library/logic/core/instances.lean
@@ -5,7 +5,7 @@
 -- logic.core.instances
 -- ====================
 
-import logic.core.connectives struc.relation
+import logic.core.connectives algebra.relation
 
 namespace relation
 
diff --git a/library/logic/logic.md b/library/logic/logic.md
index 815ae19ec0..8a74e1abd5 100644
--- a/library/logic/logic.md
+++ b/library/logic/logic.md
@@ -4,8 +4,6 @@ logic
 Logical constructions and axioms. By default, `import logic` does not
 import any additional axioms.
 
-* [core](core/core.md) : logical connectives
+* [core](core/core.md) : logical connectives and type classes
 * [axioms](axioms/axioms.md) : additional axioms
-* [classes](classes/classes.md) : classes for inhabited types, 
-decidable types, etc.  
 * [examples](examples/examples.md)
\ No newline at end of file
diff --git a/tests/lean/run/cat.lean b/tests/lean/run/cat.lean
index 52207445f0..334ad154fe 100644
--- a/tests/lean/run/cat.lean
+++ b/tests/lean/run/cat.lean
@@ -5,7 +5,7 @@
 -- category
 import logic.core.eq logic.core.connectives
 import data.unit data.sigma data.prod
-import struc.function
+import algebra.function
 
 inductive category [class] (ob : Type) (mor : ob → ob → Type) : Type :=
 mk : Π (comp : Π⦃A B C : ob⦄, mor B C → mor A B → mor A C)
diff --git a/tests/lean/run/coe11.lean b/tests/lean/run/coe11.lean
index b9cf657c84..e6a4023cb5 100644
--- a/tests/lean/run/coe11.lean
+++ b/tests/lean/run/coe11.lean
@@ -1,4 +1,4 @@
-import data.category
+import algebra.category
 open category
 
 inductive my_functor {obC obD : Type} (C : category obC) (D : category obD) : Type :=
diff --git a/tests/lean/run/congr_imp_bug.lean b/tests/lean/run/congr_imp_bug.lean
index a53e1dadde..46a4ab03dc 100644
--- a/tests/lean/run/congr_imp_bug.lean
+++ b/tests/lean/run/congr_imp_bug.lean
@@ -3,7 +3,7 @@
 --- Released under Apache 2.0 license as described in the file LICENSE.
 --- Author: Jeremy Avigad
 ----------------------------------------------------------------------------------------------------
-import logic.core.connectives struc.function
+import logic.core.connectives algebra.function
 open function
 
 namespace congr
diff --git a/tests/lean/run/div2.lean b/tests/lean/run/div2.lean
index a9439eafb7..6c26d19430 100644
--- a/tests/lean/run/div2.lean
+++ b/tests/lean/run/div2.lean
@@ -1,4 +1,4 @@
-import logic data.nat.sub struc.relation data.prod
+import logic data.nat.sub algebra.relation data.prod
 import tools.fake_simplifier
 
 open nat relation relation.iff_ops prod
diff --git a/tests/lean/run/elab_bug1.lean b/tests/lean/run/elab_bug1.lean
index bde9bdd5b7..53e80334d9 100644
--- a/tests/lean/run/elab_bug1.lean
+++ b/tests/lean/run/elab_bug1.lean
@@ -4,7 +4,7 @@
 --- Author: Jeremy Avigad
 ----------------------------------------------------------------------------------------------------
 
-import logic struc.function
+import logic algebra.function
 open eq
 open function
 
diff --git a/tests/lean/run/fun.lean b/tests/lean/run/fun.lean
index 6cca45f94d..689e5be048 100644
--- a/tests/lean/run/fun.lean
+++ b/tests/lean/run/fun.lean
@@ -1,4 +1,4 @@
-import logic struc.function
+import logic algebra.function
 open function bool
 
 
diff --git a/tests/lean/run/rel.lean b/tests/lean/run/rel.lean
index 9221b81624..bcc221ce06 100644
--- a/tests/lean/run/rel.lean
+++ b/tests/lean/run/rel.lean
@@ -1,4 +1,4 @@
-import logic struc.relation
+import logic algebra.relation
 open relation
 
 namespace is_equivalence
diff --git a/tests/lean/slow/nat_bug2.lean b/tests/lean/slow/nat_bug2.lean
index 5de70078ae..c50f6c2618 100644
--- a/tests/lean/slow/nat_bug2.lean
+++ b/tests/lean/slow/nat_bug2.lean
@@ -3,7 +3,7 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Floris van Doorn
 ----------------------------------------------------------------------------------------------------
-import logic struc.binary
+import logic algebra.binary
 open tactic binary eq_ops eq
 open decidable
 
diff --git a/tests/lean/slow/nat_wo_hints.lean b/tests/lean/slow/nat_wo_hints.lean
index 5823e1dc56..0ceb8de329 100644
--- a/tests/lean/slow/nat_wo_hints.lean
+++ b/tests/lean/slow/nat_wo_hints.lean
@@ -3,7 +3,7 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Floris van Doorn
 ----------------------------------------------------------------------------------------------------
-import logic struc.binary
+import logic algebra.binary
 open tactic binary eq_ops eq
 open decidable