From af6ee4ad9d501606445f9d574b56822644a5bb3c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 2 Dec 2016 11:24:43 -0800
Subject: [PATCH] refactor(library/init): move algebra to its own folder

---
 library/init/{algebra.lean => algebra/default.lean} | 2 +-
 library/init/{ => algebra}/group.lean               | 0
 library/init/{ => algebra}/norm_num.lean            | 2 +-
 library/init/{ => algebra}/order.lean               | 0
 library/init/{ => algebra}/ordered_group.lean       | 2 +-
 library/init/{ => algebra}/ordered_ring.lean        | 2 +-
 library/init/{ => algebra}/ring.lean                | 2 +-
 library/init/default.lean                           | 2 +-
 library/init/nat.lean                               | 1 -
 9 files changed, 6 insertions(+), 7 deletions(-)
 rename library/init/{algebra.lean => algebra/default.lean} (59%)
 rename library/init/{ => algebra}/group.lean (100%)
 rename library/init/{ => algebra}/norm_num.lean (99%)
 rename library/init/{ => algebra}/order.lean (100%)
 rename library/init/{ => algebra}/ordered_group.lean (99%)
 rename library/init/{ => algebra}/ordered_ring.lean (99%)
 rename library/init/{ => algebra}/ring.lean (99%)

diff --git a/library/init/algebra.lean b/library/init/algebra/default.lean
similarity index 59%
rename from library/init/algebra.lean
rename to library/init/algebra/default.lean
index 811eb1e382..8681a47dea 100644
--- a/library/init/algebra.lean
+++ b/library/init/algebra/default.lean
@@ -4,4 +4,4 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.group init.ordered_group init.ring init.ordered_ring
+import init.algebra.group init.algebra.ordered_group init.algebra.ring init.algebra.ordered_ring init.algebra.norm_num
diff --git a/library/init/group.lean b/library/init/algebra/group.lean
similarity index 100%
rename from library/init/group.lean
rename to library/init/algebra/group.lean
diff --git a/library/init/norm_num.lean b/library/init/algebra/norm_num.lean
similarity index 99%
rename from library/init/norm_num.lean
rename to library/init/algebra/norm_num.lean
index ce18b90a64..33573967b3 100644
--- a/library/init/norm_num.lean
+++ b/library/init/algebra/norm_num.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robert Lewis and Leonardo de Moura
 -/
 prelude
-import init.ring
+import init.algebra.ring
 
 namespace norm_num
 universe variable u
diff --git a/library/init/order.lean b/library/init/algebra/order.lean
similarity index 100%
rename from library/init/order.lean
rename to library/init/algebra/order.lean
diff --git a/library/init/ordered_group.lean b/library/init/algebra/ordered_group.lean
similarity index 99%
rename from library/init/ordered_group.lean
rename to library/init/algebra/ordered_group.lean
index 5fd6ccf091..1d60509089 100644
--- a/library/init/ordered_group.lean
+++ b/library/init/algebra/ordered_group.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura
 -/
 prelude
-import init.group
+import init.algebra.order init.algebra.group
 
 /- Make sure instances defined in this file have lower priority than the ones
    defined for concrete structures -/
diff --git a/library/init/ordered_ring.lean b/library/init/algebra/ordered_ring.lean
similarity index 99%
rename from library/init/ordered_ring.lean
rename to library/init/algebra/ordered_ring.lean
index ef84f3b7f2..42beca9c0d 100644
--- a/library/init/ordered_ring.lean
+++ b/library/init/algebra/ordered_ring.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura
 -/
 prelude
-import init.ordered_group init.ring
+import init.algebra.ordered_group init.algebra.ring
 
 /- Make sure instances defined in this file have lower priority than the ones
    defined for concrete structures -/
diff --git a/library/init/ring.lean b/library/init/algebra/ring.lean
similarity index 99%
rename from library/init/ring.lean
rename to library/init/algebra/ring.lean
index 4be5b674cf..f715952b4a 100644
--- a/library/init/ring.lean
+++ b/library/init/algebra/ring.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura
 -/
 prelude
-import init.group
+import init.algebra.group
 
 /- Make sure instances defined in this file have lower priority than the ones
    defined for concrete structures -/
diff --git a/library/init/default.lean b/library/init/default.lean
index c8d58969df..c886868af8 100644
--- a/library/init/default.lean
+++ b/library/init/default.lean
@@ -12,5 +12,5 @@ import init.monad init.option init.state init.fin init.list init.char init.strin
 import init.monad_combinators init.set
 import init.timeit init.trace init.unsigned init.ordering init.list_classes init.coe
 import init.wf init.nat_div init.meta init.instances init.breakpoint
-import init.sigma_lex init.id_locked init.order init.algebra
+import init.sigma_lex init.id_locked init.algebra
 import init.nat_lemmas init.char_lemmas init.string_lemmas
diff --git a/library/init/nat.lean b/library/init/nat.lean
index 87495229e6..0e06c6c97b 100644
--- a/library/init/nat.lean
+++ b/library/init/nat.lean
@@ -5,7 +5,6 @@ Authors: Floris van Doorn, Leonardo de Moura
 -/
 prelude
 import init.relation init.num
-import init.order
 
 notation `ℕ` := nat