chore: cleanup imports (leanprover#5825)

opencompl · Oct 27, 2024 · 0d7f32a · 0d7f32a
1 parent 8a2351b
commit 0d7f32a
Show file tree

Hide file tree

Showing 11 changed files with 6 additions and 25 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -7,6 +7,7 @@ prelude
 import Lean.Meta.Basic
 import Lean.Data.Json
 import Lean.Data.RBMap
+import Init.Control.Option
 
 namespace Lean
-Original file line number
+Diff line change
@@ Expand Up / @@ -5,6 +5,7 @@ Authors: Leonardo de Moura @@
     -/
     prelude
     import Lean.Meta.Basic
+    import Init.Control.Option
     namespace Lean.Meta
@@ Expand Down @@