chore: import cleanup in Init (#6522)

This PR avoids unnecessarily importing "kitchen sink" files.
leanprover · Jan 4, 2025 · 9080df3 · 9080df3
1 parent cdeb958
commit 9080df3
Show file tree

Hide file tree

Showing 9 changed files with 5 additions and 8 deletions.
diff --git a/src/Lean/Data/Lsp/Utf16.lean b/src/Lean/Data/Lsp/Utf16.lean
@@ -6,7 +6,6 @@ Authors: Marc Huisinga, Wojciech Nawrocki
 -/
 prelude
 import Init.Data.String
-import Init.Data.Array
 import Lean.Data.Lsp.Basic
 import Lean.Data.Position
 import Lean.DeclarationRange

diff --git a/src/Lean/Linter/MissingDocs.lean b/src/Lean/Linter/MissingDocs.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 prelude
+import Lean.Parser.Syntax
 import Lean.Meta.Tactic.Simp.RegisterCommand
 import Lean.Elab.Command
 import Lean.Elab.SetOption

diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sebastian Ullrich, Leonardo de Moura, Gabriel Ebner, Mario Carneiro
 -/
 prelude
-import Lean.Parser
 import Lean.PrettyPrinter.Delaborator.Attributes
 import Lean.PrettyPrinter.Delaborator.Basic
 import Lean.PrettyPrinter.Delaborator.SubExpr

diff --git a/src/Lean/Server/Completion.lean b/src/Lean/Server/Completion.lean
@@ -5,6 +5,7 @@ Authors: Leonardo de Moura, Marc Huisinga
 -/
 prelude
 import Lean.Server.Completion.CompletionCollectors
+import Std.Data.HashMap
 
 namespace Lean.Server.Completion
 open Lsp

diff --git a/src/Lean/Util/ShareCommon.lean b/src/Lean/Util/ShareCommon.lean
@@ -5,8 +5,8 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.ShareCommon
-import Std.Data.HashSet
-import Std.Data.HashMap
+import Std.Data.HashSet.Basic
+import Std.Data.HashMap.Basic
 import Lean.Data.PersistentHashMap
 import Lean.Data.PersistentHashSet
 

diff --git a/src/Std/Sat/AIG/Basic.lean b/src/Std/Sat/AIG/Basic.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
 prelude
-import Std.Data.HashMap
 import Std.Data.HashSet
 
 namespace Std

diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Implementation.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Implementation.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Josh Clune
 -/
 prelude
-import Init.Data.Array
 import Std.Tactic.BVDecide.LRAT.Internal.Formula.Class
 import Std.Tactic.BVDecide.LRAT.Internal.Assignment
 import Std.Sat.CNF.Basic

diff --git a/src/Std/Time/DateTime/Timestamp.lean b/src/Std/Time/DateTime/Timestamp.lean
@@ -5,7 +5,6 @@ Authors: Sofia Rodrigues
 -/
 prelude
 import Std.Time.Internal
-import Init.Data.Int
 import Init.System.IO
 import Std.Time.Time
 import Std.Time.Date

diff --git a/src/Std/Time/Internal/Bounded.lean b/src/Std/Time/Internal/Bounded.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sofia Rodrigues
 -/
 prelude
-import Init.Data.Int
+import Init.Omega
 
 namespace Std
 namespace Time