refactor: dependencies

src/Init/Data/Int/Basic.lean

@@ -6,10 +6,9 @@ Authors: Jeremy Avigad, Leonardo de Moura
 The integers, with addition, multiplication, and subtraction.
 -/
 prelude
-import Init.Data.Nat.Basic
-import Init.Data.List
-import Init.Data.Repr
-import Init.Data.ToString.Basic
+import Init.Coe
+import Init.Data.Nat.Div
+import Init.Data.List.Basic
 open Nat
 
 /- the Type, coercions, and notation -/
@@ -125,16 +124,6 @@ def natAbs (m : @& Int) : Nat :=
   | ofNat m   => m
   | negSucc m => m.succ
 
-protected def repr : Int → String
-  | ofNat m   => Nat.repr m
-  | negSucc m => "-" ++ Nat.repr (succ m)
-
-instance : Repr Int where
-  repr := Int.repr
-
-instance : ToString Int where
-  toString := Int.repr
-
 instance : OfNat Int n where
   ofNat := Int.ofNat n
 
@@ -172,25 +161,3 @@ instance : HPow Int Nat Int where
   hPow := Int.pow
 
 end Int
-
-namespace String
-
-def toInt? (s : String) : Option Int :=
-  if s.get 0 = '-' then do
-    let v ← (s.toSubstring.drop 1).toNat?;
-    pure <| - Int.ofNat v
-  else
-   Int.ofNat <$> s.toNat?
-
-def isInt (s : String) : Bool :=
-  if s.get 0 = '-' then
-    (s.toSubstring.drop 1).isNat
-  else
-    s.isNat
-
-def toInt! (s : String) : Int :=
-  match s.toInt? with
-  | some v => v
-  | none   => panic! "Int expected"
-
-end String

src/Init/Data/Repr.lean

@@ -5,8 +5,9 @@ Author: Leonardo de Moura
 -/
 prelude
 import Init.Data.String.Basic
-import Init.Data.UInt
+import Init.Data.Int.Basic
 import Init.Data.Nat.Div
+import Init.Data.UInt
 import Init.Control.Id
 open Sum Subtype Nat
 
@@ -135,6 +136,13 @@ end Nat
 instance : Repr Nat :=
   ⟨Nat.repr⟩
 
+protected def Int.repr : Int → String
+  | ofNat m   => Nat.repr m
+  | negSucc m => "-" ++ Nat.repr (succ m)
+
+instance : Repr Int where
+  repr := Int.repr
+
 def hexDigitRepr (n : Nat) : String :=
   String.singleton <| Nat.digitChar n
 

src/Init/Data/ToString/Basic.lean

@@ -8,6 +8,7 @@ import Init.Data.String.Basic
 import Init.Data.UInt
 import Init.Data.Nat.Div
 import Init.Data.Repr
+import Init.Data.Int.Basic
 import Init.Control.Id
 open Sum Subtype Nat
 
@@ -67,6 +68,11 @@ instance : ToString Unit :=
 instance : ToString Nat :=
   ⟨fun n => repr n⟩
 
+instance : ToString Int where
+  toString
+    | Int.ofNat m   => toString m
+    | Int.negSucc m => "-" ++ toString (succ m)
+
 instance : ToString Char :=
   ⟨fun c => c.toString⟩
 
@@ -109,3 +115,21 @@ instance {α : Type u} {β : α → Type v} [ToString α] [s : ∀ x, ToString (
 
 instance {α : Type u} {p : α → Prop} [ToString α] : ToString (Subtype p) := ⟨fun s =>
   toString (val s)⟩
+
+def String.toInt? (s : String) : Option Int :=
+  if s.get 0 = '-' then do
+    let v ← (s.toSubstring.drop 1).toNat?;
+    pure <| - Int.ofNat v
+  else
+   Int.ofNat <$> s.toNat?
+
+def String.isInt (s : String) : Bool :=
+  if s.get 0 = '-' then
+    (s.toSubstring.drop 1).isNat
+  else
+    s.isNat
+
+def String.toInt! (s : String) : Int :=
+  match s.toInt? with
+  | some v => v
+  | none   => panic "Int expected"