From 0d7f32af67aa8a4925be05ceae705bd765524624 Mon Sep 17 00:00:00 2001
From: Kim Morrison <scott.morrison@gmail.com>
Date: Thu, 24 Oct 2024 10:51:13 +1100
Subject: [PATCH] chore: cleanup imports (#5825)

---
 src/Init/Control/StateRef.lean    | 3 +--
 src/Init/Data/Option/Basic.lean   | 2 --
 src/Init/Data/Repr.lean           | 4 ----
 src/Init/Data/String/Basic.lean   | 1 -
 src/Init/Data/ToString/Basic.lean | 9 ++-------
 src/Init/System/FilePath.lean     | 2 --
 src/Init/System/IO.lean           | 4 ----
 src/Init/System/IOError.lean      | 3 ---
 src/Lean/Meta/LitValues.lean      | 1 +
 src/Lean/Meta/Offset.lean         | 1 +
 src/Lean/SubExpr.lean             | 1 +
 11 files changed, 6 insertions(+), 25 deletions(-)

diff --git a/src/Init/Control/StateRef.lean b/src/Init/Control/StateRef.lean
index b4185766a11f..6aa41d8c273a 100644
--- a/src/Init/Control/StateRef.lean
+++ b/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 α
 
diff --git a/src/Init/Data/Option/Basic.lean b/src/Init/Data/Option/Basic.lean
index 73a7d574bae6..a4ee792f62c7 100644
--- a/src/Init/Data/Option/Basic.lean
+++ b/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
 
diff --git a/src/Init/Data/Repr.lean b/src/Init/Data/Repr.lean
index 9b363da289e1..50123a9ac6bb 100644
--- a/src/Init/Data/Repr.lean
+++ b/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
diff --git a/src/Init/Data/String/Basic.lean b/src/Init/Data/String/Basic.lean
index 95fffe785c87..6851c3ef1334 100644
--- a/src/Init/Data/String/Basic.lean
+++ b/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
 
diff --git a/src/Init/Data/ToString/Basic.lean b/src/Init/Data/ToString/Basic.lean
index 06b3d85ff09b..57e777bf3301 100644
--- a/src/Init/Data/ToString/Basic.lean
+++ b/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
diff --git a/src/Init/System/FilePath.lean b/src/Init/System/FilePath.lean
index 4a8c5dc76d1f..18f9d6321327 100644
--- a/src/Init/System/FilePath.lean
+++ b/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
diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean
index f391dedec4fc..15b0d8c58391 100644
--- a/src/Init/System/IO.lean
+++ b/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
diff --git a/src/Init/System/IOError.lean b/src/Init/System/IOError.lean
index 4e76bb964ee1..4068503078c1 100644
--- a/src/Init/System/IOError.lean
+++ b/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:
diff --git a/src/Lean/Meta/LitValues.lean b/src/Lean/Meta/LitValues.lean
index 19b8efe3783a..0bc7acd03a21 100644
--- a/src/Lean/Meta/LitValues.lean
+++ b/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
 
diff --git a/src/Lean/Meta/Offset.lean b/src/Lean/Meta/Offset.lean
index eac7e1a55c6c..01216f454284 100644
--- a/src/Lean/Meta/Offset.lean
+++ b/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
diff --git a/src/Lean/SubExpr.lean b/src/Lean/SubExpr.lean
index 567b7da20dca..309eda5857c3 100644
--- a/src/Lean/SubExpr.lean
+++ b/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