refactor(data/num/string): break into pieces to reduce dependencies

library/data/num/decl.lean

@@ -3,7 +3,7 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura
 ----------------------------------------------------------------------------------------------------
-
+import data.unit.decl
 -- pos_num and num are two auxiliary datatypes used when parsing numerals such as 13, 0, 26.
 -- The parser will generate the terms (pos (bit1 (bit1 (bit0 one)))), zero, and (pos (bit0 (bit1 (bit1 one)))).
 -- This representation can be coerced in whatever we want (e.g., naturals, integers, reals, etc).

library/data/string/decl.lean

@@ -0,0 +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 data.bool.decl
+
+inductive char : Type :=
+  mk : bool → bool → bool → bool → bool → bool → bool → bool → char
+
+inductive string : Type :=
+  empty : string,
+  str   : char → string → string

library/data/string/default.lean

@@ -0,0 +1,4 @@
+-- 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 data.string.decl data.string.thms

library/data/string/thms.lean

@@ -1,23 +1,14 @@
 -- 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 data.bool
-
+import data.string.decl data.bool
 open bool inhabited
 
-inductive char : Type :=
-  mk : bool → bool → bool → bool → bool → bool → bool → bool → char
-
 namespace char
   protected definition is_inhabited [instance] : inhabited char :=
   inhabited.mk (mk ff ff ff ff ff ff ff ff)
 end char
 
-inductive string : Type :=
-  empty : string,
-  str   : char → string → string
-
 namespace string
   protected definition is_inhabited [instance] : inhabited string :=
   inhabited.mk empty

library/tools/helper_tactics.lean

@@ -7,7 +7,7 @@
 
 -- Useful tactics.
 
-import .tactic
+import tools.tactic logic.eq
 
 open tactic
 

library/tools/tactic.lean

@@ -3,8 +3,7 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura
 ----------------------------------------------------------------------------------------------------
-
-import data.string data.num.decl
+import data.string.decl data.num.decl
 -- This is just a trick to embed the 'tactic language' as a
 -- Lean expression. We should view 'tactic' as automation
 -- that when execute produces a term.

tests/lean/beginend_bug.lean

@@ -1,4 +1,4 @@
-import tools.tactic
+import tools.tactic logic
 open tactic
 
 theorem foo (A : Type) (a b c : A) (Hab : a = b) (Hbc : b = c) : a = c :=

tests/lean/goals1.lean

@@ -1,4 +1,4 @@
-import tools.tactic
+import tools.tactic logic.eq
 open tactic
 set_option pp.notation false
 

tests/lean/run/beginend.lean

@@ -1,4 +1,4 @@
-import tools.tactic
+import tools.tactic logic.eq
 open tactic
 
 theorem foo (A : Type) (a b c : A) (Hab : a = b) (Hbc : b = c) : a = c :=

tests/lean/run/beginend3.lean

@@ -1,4 +1,4 @@
-import tools.tactic
+import tools.tactic logic
 open tactic
 
 theorem foo (A : Type) (a b c : A) : a = b → b = c → a = c ∧ c = a :=

tests/lean/run/decidable.lean

@@ -1,4 +1,4 @@
-import logic data.unit
+import logic data.unit data.bool
 open bool unit decidable
 
 constants a b c : bool

tests/lean/run/rename_tac.lean

@@ -1,4 +1,4 @@
-import tools.tactic
+import tools.tactic logic
 open tactic
 
 theorem foo (A : Type) (a b c : A) (Hab : a = b) (Hbc : b = c) : a = c :=

tests/lean/run/set2.lean

@@ -1,4 +1,4 @@
-import logic
+import logic data.bool
 open bool
 
 namespace set

tests/lean/run/tac1.lean

@@ -1,4 +1,4 @@
-import tools.tactic
+import tools.tactic logic
 open tactic
 
 definition mytac := apply @and.intro; apply @eq.refl