chore: import cleanup in Init (#6522)
This PR avoids unnecessarily importing "kitchen sink" files.
This commit is contained in:
parent
cdeb958afd
commit
9080df3110
9 changed files with 5 additions and 8 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue