refactor(library/init): move combinator logic to core

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 -/

library/init/combinator.lean

@@ -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

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

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

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

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