chore: cleanup imports

src/Init/Control/StateRef.lean

@@ -6,8 +6,7 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 The State monad transformer using IO references.
 -/
 prelude
-import Init.System.IO
-import Init.Control.State
+import Init.System.ST
 
 def StateRefT' (ω : Type) (σ : Type) (m : Type → Type) (α : Type) : Type := ReaderT (ST.Ref ω σ) m α
 

src/Init/Data/Option/Basic.lean

@@ -4,9 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Mario Carneiro
 -/
 prelude
-import Init.Core
 import Init.Control.Basic
-import Init.Coe
 
 namespace Option
 

src/Init/Data/Repr.lean

@@ -5,10 +5,6 @@ Author: Leonardo de Moura
 -/
 prelude
 import Init.Data.Format.Basic
-import Init.Data.Int.Basic
-import Init.Data.Nat.Div
-import Init.Data.UInt.BasicAux
-import Init.Control.Id
 open Sum Subtype Nat
 
 open Std

src/Init/Data/String/Basic.lean

@@ -6,7 +6,6 @@ Author: Leonardo de Moura, Mario Carneiro
 prelude
 import Init.Data.List.Basic
 import Init.Data.Char.Basic
-import Init.Data.Option.Basic
 
 universe u
 

src/Init/Data/ToString/Basic.lean

@@ -4,14 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
 prelude
-import Init.Data.String.Basic
-import Init.Data.UInt.BasicAux
-import Init.Data.Nat.Div
 import Init.Data.Repr
-import Init.Data.Int.Basic
-import Init.Data.Format.Basic
-import Init.Control.Id
-import Init.Control.Option
+import Init.Data.Option.Basic
+
 open Sum Subtype Nat
 
 open Std

src/Init/System/FilePath.lean

@@ -5,8 +5,6 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 prelude
 import Init.System.Platform
-import Init.Data.String.Basic
-import Init.Data.Repr
 import Init.Data.ToString.Basic
 
 namespace System

src/Init/System/IO.lean

@@ -4,13 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Luke Nelson, Jared Roesch, Leonardo de Moura, Sebastian Ullrich, Mac Malone
 -/
 prelude
-import Init.Control.Reader
-import Init.Data.String
-import Init.Data.ByteArray
 import Init.System.IOError
 import Init.System.FilePath
 import Init.System.ST
-import Init.Data.ToString.Macro
 import Init.Data.Ord
 
 open System

src/Init/System/IOError.lean

@@ -5,10 +5,7 @@ Authors: Simon Hudon
 -/
 
 prelude
-import Init.Core
-import Init.Data.UInt.Basic
 import Init.Data.ToString.Basic
-import Init.Data.String.Basic
 
 /--
 Imitate the structure of IOErrorType in Haskell:

src/Lean/Meta/LitValues.lean

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.Meta.Basic
+import Init.Control.Option
 
 namespace Lean.Meta
 

src/Lean/Meta/Offset.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
+import Init.Control.Option
 import Lean.Data.LBool
 import Lean.Meta.InferType
 import Lean.Meta.NatInstTesters

src/Lean/SubExpr.lean

@@ -7,6 +7,7 @@ prelude
 import Lean.Meta.Basic
 import Lean.Data.Json
 import Lean.Data.RBMap
+import Init.Control.Option
 
 namespace Lean