refactor(library): rename algebra directory to struc, move categories.lean to algebra

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)

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
 

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

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

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

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

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
 

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
 

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

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
 

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
 

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
 

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

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
 

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)

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)

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 :=

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

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

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
 

tests/lean/run/fun.lean

@@ -1,4 +1,4 @@
-import logic struc.function
+import logic algebra.function
 open function bool
 
 

tests/lean/run/rel.lean

@@ -1,4 +1,4 @@
-import logic struc.relation
+import logic algebra.relation
 open relation
 
 namespace is_equivalence

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
 

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