From b254c78c441b09ffea7b491d314256fc2c2b39b7 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 2 Mar 2015 18:45:08 -0800
Subject: [PATCH] refactor(library/algebra): move bundled structures to
 separate module

Motivation: performance.
After this commit, the bundled instances do not participate in the
class/instance resolution if we do not import algebra.bundled.
---
 library/algebra/bundled.lean | 84 ++++++++++++++++++++++++++++++++++++
 library/algebra/group.lean   | 74 -------------------------------
 tests/lean/438.lean          |  2 +-
 3 files changed, 85 insertions(+), 75 deletions(-)
 create mode 100644 library/algebra/bundled.lean

diff --git a/library/algebra/bundled.lean b/library/algebra/bundled.lean
new file mode 100644
index 000000000..ea41110d5
--- /dev/null
+++ b/library/algebra/bundled.lean
@@ -0,0 +1,84 @@
+/-
+Copyright (c) 2015 Jeremy Avigad. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Module: algebra.bundled
+Authors: Jeremy Avigad
+
+Bundled structures
+-/
+import algebra.group
+
+namespace algebra
+structure Semigroup :=
+(carrier : Type) (struct : semigroup carrier)
+
+attribute Semigroup.carrier [coercion]
+attribute Semigroup.struct [instance]
+
+structure CommSemigroup :=
+(carrier : Type) (struct : comm_semigroup carrier)
+
+attribute CommSemigroup.carrier [coercion]
+attribute CommSemigroup.struct [instance]
+
+structure Monoid :=
+(carrier : Type) (struct : monoid carrier)
+
+attribute Monoid.carrier [coercion]
+attribute Monoid.struct [instance]
+
+structure CommMonoid :=
+(carrier : Type) (struct : comm_monoid carrier)
+
+attribute CommMonoid.carrier [coercion]
+attribute CommMonoid.struct [instance]
+
+structure Group :=
+(carrier : Type) (struct : group carrier)
+
+attribute Group.carrier [coercion]
+attribute Group.struct [instance]
+
+structure CommGroup :=
+(carrier : Type) (struct : comm_group carrier)
+
+attribute CommGroup.carrier [coercion]
+attribute CommGroup.struct [instance]
+
+structure AddSemigroup :=
+(carrier : Type) (struct : add_semigroup carrier)
+
+attribute AddSemigroup.carrier [coercion]
+attribute AddSemigroup.struct [instance]
+
+structure AddCommSemigroup :=
+(carrier : Type) (struct : add_comm_semigroup carrier)
+
+attribute AddCommSemigroup.carrier [coercion]
+attribute AddCommSemigroup.struct [instance]
+
+structure AddMonoid :=
+(carrier : Type) (struct : add_monoid carrier)
+
+attribute AddMonoid.carrier [coercion]
+attribute AddMonoid.struct [instance]
+
+structure AddCommMonoid :=
+(carrier : Type) (struct : add_comm_monoid carrier)
+
+attribute AddCommMonoid.carrier [coercion]
+attribute AddCommMonoid.struct [instance]
+
+structure AddGroup :=
+(carrier : Type) (struct : add_group carrier)
+
+attribute AddGroup.carrier [coercion]
+attribute AddGroup.struct [instance]
+
+structure AddCommGroup :=
+(carrier : Type) (struct : add_comm_group carrier)
+
+attribute AddCommGroup.carrier [coercion]
+attribute AddCommGroup.struct [instance]
+end algebra
diff --git a/library/algebra/group.lean b/library/algebra/group.lean
index 75ce82bb4..06f915bdb 100644
--- a/library/algebra/group.lean
+++ b/library/algebra/group.lean
@@ -469,78 +469,4 @@ section add_comm_group
   !add.comm ▸ add_eq_of_eq_sub H
 end add_comm_group
 
-/- bundled structures -/
-
-structure Semigroup :=
-(carrier : Type) (struct : semigroup carrier)
-
-attribute Semigroup.carrier [coercion]
-attribute Semigroup.struct [instance]
-
-structure CommSemigroup :=
-(carrier : Type) (struct : comm_semigroup carrier)
-
-attribute CommSemigroup.carrier [coercion]
-attribute CommSemigroup.struct [instance]
-
-structure Monoid :=
-(carrier : Type) (struct : monoid carrier)
-
-attribute Monoid.carrier [coercion]
-attribute Monoid.struct [instance]
-
-structure CommMonoid :=
-(carrier : Type) (struct : comm_monoid carrier)
-
-attribute CommMonoid.carrier [coercion]
-attribute CommMonoid.struct [instance]
-
-structure Group :=
-(carrier : Type) (struct : group carrier)
-
-attribute Group.carrier [coercion]
-attribute Group.struct [instance]
-
-structure CommGroup :=
-(carrier : Type) (struct : comm_group carrier)
-
-attribute CommGroup.carrier [coercion]
-attribute CommGroup.struct [instance]
-
-structure AddSemigroup :=
-(carrier : Type) (struct : add_semigroup carrier)
-
-attribute AddSemigroup.carrier [coercion]
-attribute AddSemigroup.struct [instance]
-
-structure AddCommSemigroup :=
-(carrier : Type) (struct : add_comm_semigroup carrier)
-
-attribute AddCommSemigroup.carrier [coercion]
-attribute AddCommSemigroup.struct [instance]
-
-structure AddMonoid :=
-(carrier : Type) (struct : add_monoid carrier)
-
-attribute AddMonoid.carrier [coercion]
-attribute AddMonoid.struct [instance]
-
-structure AddCommMonoid :=
-(carrier : Type) (struct : add_comm_monoid carrier)
-
-attribute AddCommMonoid.carrier [coercion]
-attribute AddCommMonoid.struct [instance]
-
-structure AddGroup :=
-(carrier : Type) (struct : add_group carrier)
-
-attribute AddGroup.carrier [coercion]
-attribute AddGroup.struct [instance]
-
-structure AddCommGroup :=
-(carrier : Type) (struct : add_comm_group carrier)
-
-attribute AddCommGroup.carrier [coercion]
-attribute AddCommGroup.struct [instance]
-
 end algebra
diff --git a/tests/lean/438.lean b/tests/lean/438.lean
index 186547d34..fa093f1f1 100644
--- a/tests/lean/438.lean
+++ b/tests/lean/438.lean
@@ -1,4 +1,4 @@
-import algebra.group
+import algebra.bundled
 open algebra
 
 attribute Group.struct [coercion]