From fb38b6e01696fea07cc0c88ff65d469cd4e1b6e7 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 2 Dec 2016 15:56:52 -0800
Subject: [PATCH] refactor(library/init): move combinator logic to core

---
 library/init/algebra/group.lean               |  2 +-
 library/init/combinator.lean                  | 13 -------------
 library/init/core.lean                        |  8 ++++++++
 library/init/data/basic.lean                  |  2 +-
 library/init/data/sigma/lex.lean              |  2 +-
 library/init/meta/mk_has_sizeof_instance.lean |  3 +--
 6 files changed, 12 insertions(+), 18 deletions(-)
 delete mode 100644 library/init/combinator.lean

diff --git a/library/init/algebra/group.lean b/library/init/algebra/group.lean
index c203271d38..c4328bde92 100644
--- a/library/init/algebra/group.lean
+++ b/library/init/algebra/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.logic init.binary init.combinator init.meta.interactive init.meta.decl_cmds
+import init.logic init.binary init.meta.interactive init.meta.decl_cmds
 
 /- Make sure instances defined in this file have lower priority than the ones
    defined for concrete structures -/
diff --git a/library/init/combinator.lean b/library/init/combinator.lean
deleted file mode 100644
index 030a37bb90..0000000000
--- a/library/init/combinator.lean
+++ /dev/null
@@ -1,13 +0,0 @@
-/-
-Copyright (c) 2016 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-/- Combinator calculus -/
-namespace combinator
-universe variables u₁ u₂ u₃
-def I {α : Type u₁} (a : α) := a
-def K {α : Type u₁} {β : Type u₂} (a : α) (b : β) := a
-def S {α : Type u₁} {β : Type u₂} {γ : Type u₃} (x : α → β → γ) (y : α → β) (z : α) := x z (y z)
-end combinator
diff --git a/library/init/core.lean b/library/init/core.lean
index 00816a06e0..2f569b7ce7 100644
--- a/library/init/core.lean
+++ b/library/init/core.lean
@@ -565,3 +565,11 @@ rfl
 
 attribute [simp.sizeof]
 lemma nat_add_zero (n : nat) : n + 0 = n := rfl
+
+/- Combinator calculus -/
+namespace combinator
+universe variables u₁ u₂ u₃
+def I {α : Type u₁} (a : α) := a
+def K {α : Type u₁} {β : Type u₂} (a : α) (b : β) := a
+def S {α : Type u₁} {β : Type u₂} {γ : Type u₃} (x : α → β → γ) (y : α → β) (z : α) := x z (y z)
+end combinator
diff --git a/library/init/data/basic.lean b/library/init/data/basic.lean
index ff5b382390..114ddf0dd2 100644
--- a/library/init/data/basic.lean
+++ b/library/init/data/basic.lean
@@ -4,6 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.data.setoid init.data.quot init.data.bool.basic init.data.unit init.data.nat.basic init.data.prod init.data.sum.basic init.combinator
+import init.data.setoid init.data.quot init.data.bool.basic init.data.unit init.data.nat.basic init.data.prod init.data.sum.basic
 import init.data.num.basic init.data.sigma.basic init.data.subtype init.data.fin.basic init.data.list.basic init.data.char.basic init.data.string.basic
 import init.data.option.basic init.data.set init.data.unsigned init.data.ordering init.data.list.classes init.data.to_string
diff --git a/library/init/data/sigma/lex.lean b/library/init/data/sigma/lex.lean
index 5e65aa0f3e..e18404ebb1 100644
--- a/library/init/data/sigma/lex.lean
+++ b/library/init/data/sigma/lex.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
 prelude
-import init.data.sigma.basic init.meta init.combinator
+import init.data.sigma.basic init.meta
 universe variables u v
 namespace sigma
 section
diff --git a/library/init/meta/mk_has_sizeof_instance.lean b/library/init/meta/mk_has_sizeof_instance.lean
index cd1a975f95..0acbf28b85 100644
--- a/library/init/meta/mk_has_sizeof_instance.lean
+++ b/library/init/meta/mk_has_sizeof_instance.lean
@@ -6,8 +6,7 @@ Authors: Leonardo de Moura
 Helper tactic for constructing has_sizeof instance.
 -/
 prelude
-import init.meta.rec_util init.combinator
-import init.meta.constructor_tactic
+import init.meta.rec_util init.meta.constructor_tactic
 
 namespace tactic
 open expr environment list