chore: reduce imports (#533)

Co-authored-by: Mario Carneiro <[email protected]>
leanprover-community · Jan 17, 2024 · ee4a0f1 · ee4a0f1
1 parent 8d34048
commit ee4a0f1
Show file tree

Hide file tree

Showing 30 changed files with 31 additions and 32 deletions.
diff --git a/Std/CodeAction/Basic.lean b/Std/CodeAction/Basic.lean
@@ -5,7 +5,6 @@ Authors: Mario Carneiro
 -/
 import Lean.Elab.BuiltinTerm
 import Lean.Elab.BuiltinNotation
-import Std.Lean.Name
 import Std.Lean.InfoTree
 import Std.CodeAction.Attr
 

diff --git a/Std/CodeAction/Misc.lean b/Std/CodeAction/Misc.lean
@@ -3,9 +3,11 @@ Copyright (c) 2023 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
+import Lean.Elab.BuiltinTerm
+import Lean.Elab.BuiltinNotation
 import Std.Lean.Name
 import Std.Lean.Position
-import Std.CodeAction.Basic
+import Std.CodeAction.Attr
 
 /-!
 # Miscellaneous code actions

diff --git a/Std/Control/Nondet/Basic.lean b/Std/Control/Nondet/Basic.lean
@@ -3,7 +3,7 @@ Copyright (c) 2023 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-import Std.Tactic.Lint
+import Std.Tactic.Lint.Misc
 import Std.Data.MLList.Basic
 
 /-!

diff --git a/Std/Data/Array/Init/Lemmas.lean b/Std/Data/Array/Init/Lemmas.lean
@@ -6,6 +6,7 @@ Authors: Mario Carneiro
 import Std.Tactic.NoMatch
 import Std.Tactic.HaveI
 import Std.Classes.LawfulMonad
+import Std.Data.Fin.Init.Lemmas
 import Std.Data.Nat.Init.Lemmas
 import Std.Data.List.Init.Lemmas
 import Std.Data.Array.Init.Basic

diff --git a/Std/Data/Array/Match.lean b/Std/Data/Array/Match.lean
@@ -3,8 +3,8 @@ Copyright (c) 2023 F. G. Dorais. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: F. G. Dorais
 -/
-import Std.Data.Array.Basic
-import Std.Data.Array.Lemmas
+import Std.Data.Nat.Lemmas
+import Std.Data.Array.Init.Lemmas
 
 namespace Array
 

diff --git a/Std/Data/Json.lean b/Std/Data/Json.lean
@@ -3,7 +3,7 @@
  Released under Apache 2.0 license as described in the file LICENSE.
  Authors: E.W.Ayers, Wojciech Nawrocki
 -/
-import Std.Lean.Json
+import Lean.Data.Json.FromToJson
 import Lean.Syntax
 
 /-!

diff --git a/Std/Data/List/Basic.lean b/Std/Data/List/Basic.lean
@@ -7,7 +7,6 @@ import Std.Classes.SetNotation
 import Std.Tactic.NoMatch
 import Std.Data.Option.Init.Lemmas
 import Std.Data.Array.Init.Lemmas
-import Std.Data.List.Init.Attach
 
 namespace List
 

diff --git a/Std/Data/List/Init/Lemmas.lean b/Std/Data/List/Init/Lemmas.lean
@@ -3,7 +3,6 @@ Copyright (c) 2014 Parikshit Khanna. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro
 -/
-import Std.Data.Fin.Init.Lemmas
 import Std.Classes.SetNotation
 import Std.Logic
 

diff --git a/Std/Data/List/Lemmas.lean b/Std/Data/List/Lemmas.lean
@@ -5,8 +5,7 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, M
 -/
 import Std.Control.ForInStep.Lemmas
 import Std.Data.Bool
-import Std.Data.Fin.Lemmas
-import Std.Data.Nat.Lemmas
+import Std.Data.Fin.Basic
 import Std.Data.List.Basic
 import Std.Data.Option.Lemmas
 import Std.Classes.BEq

diff --git a/Std/Data/List/Perm.lean b/Std/Data/List/Perm.lean
@@ -7,6 +7,7 @@ import Std.Tactic.Relation.Rfl
 import Std.Data.List.Lemmas
 import Std.Data.List.Count
 import Std.Data.List.Pairwise
+import Std.Data.List.Init.Attach
 
 /-!
 # List Permutations

diff --git a/Std/Data/Option/Basic.lean b/Std/Data/Option/Basic.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 import Std.Classes.SetNotation
-import Std.Classes.LawfulMonad
 import Std.Tactic.NoMatch
 
 namespace Option

diff --git a/Std/Data/Prod/Lex.lean b/Std/Data/Prod/Lex.lean
@@ -5,7 +5,6 @@ Authors: Jannis Limperg
 -/
 import Std.Tactic.LeftRight
 import Std.Tactic.RCases
-import Std.Logic
 
 namespace Prod
 

diff --git a/Std/Data/Range/Lemmas.lean b/Std/Data/Range/Lemmas.lean
@@ -1,5 +1,6 @@
 import Std.Tactic.ByCases
 import Std.Data.List.Lemmas
+import Std.Data.List.Init.Attach
 
 namespace Std.Range
 

diff --git a/Std/Data/String/Basic.lean b/Std/Data/String/Basic.lean
@@ -3,8 +3,6 @@ Copyright (c) 2022 Jannis Limperg. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jannis Limperg, James Gallicchio, F. G. Dorais
 -/
-
-import Std.Data.Char
 import Std.Data.Nat.Lemmas
 import Std.Data.Array.Match
 

diff --git a/Std/Lean/Json.lean b/Std/Lean/Json.lean
@@ -3,8 +3,7 @@
  Released under Apache 2.0 license as described in the file LICENSE.
  Authors: E.W.Ayers, Mario Carneiro
 -/
-
-import Lean.Data.Json
+import Lean.Data.Json.FromToJson
 import Std.Lean.Float
 
 open Lean

diff --git a/Std/Lean/Meta/Basic.lean b/Std/Lean/Meta/Basic.lean
@@ -3,7 +3,9 @@ Copyright (c) 2022 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Jannis Limperg
 -/
-import Lean.Meta
+import Lean.Elab.Term
+import Lean.Meta.Tactic.Apply
+import Lean.Meta.Tactic.Replace
 import Std.Lean.LocalContext
 
 open Lean Lean.Meta

diff --git a/Std/Lean/Meta/Inaccessible.lean b/Std/Lean/Meta/Inaccessible.lean
@@ -1,4 +1,9 @@
-import Lean.Meta
+/-
+Copyright (c) 2022 Jannis Limperg. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jannis Limperg
+-/
+import Lean.Meta.InferType
 
 open Lean Lean.Meta
 

diff --git a/Std/Lean/Meta/Simp.lean b/Std/Lean/Meta/Simp.lean
@@ -3,8 +3,8 @@ Copyright (c) 2022 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison, Gabriel Ebner, Floris van Doorn
 -/
+import Lean.Elab.Tactic.Simp
 import Std.Tactic.OpenPrivate
-import Std.Lean.Meta.DiscrTree
 
 /-!
 # Helper functions for using the simplifier.

diff --git a/Std/Lean/Meta/UnusedNames.lean b/Std/Lean/Meta/UnusedNames.lean
@@ -3,8 +3,6 @@ Copyright (c) 2022 Jannis Limperg. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jannis Limperg
 -/
-
-import Lean.Meta
 import Std.Data.String.Basic
 
 open Lean Lean.Meta

diff --git a/Std/Lean/System/IO.lean b/Std/Lean/System/IO.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import Std.Data.List.Lemmas
-import Std.Data.MLList.Basic
 
 /-!
 # Functions for manipulating a list of tasks

diff --git a/Std/Lean/Util/EnvSearch.lean b/Std/Lean/Util/EnvSearch.lean
@@ -3,7 +3,6 @@ Copyright (c) 2021 Shing Tak Lam. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Shing Tak Lam, Daniel Selsam, Mario Carneiro
 -/
-import Lean.Modifiers
 import Std.Tactic.Lint.Misc
 
 namespace Lean

diff --git a/Std/Tactic/Case.lean b/Std/Tactic/Case.lean
@@ -3,7 +3,7 @@ Copyright (c) 2023 Kyle Miller. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kyle Miller
 -/
-import Lean.Elab.Tactic
+import Lean.Elab.Tactic.Conv.Pattern
 
 /-!
 # Extensions to the `case` tactic

diff --git a/Std/Tactic/FalseOrByContra.lean b/Std/Tactic/FalseOrByContra.lean
@@ -3,7 +3,7 @@ Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-import Std.Lean.Expr
+import Lean.Elab.Tactic.Basic
 import Std.Lean.Meta.Basic
 
 /-!

diff --git a/Std/Tactic/Lint/Basic.lean b/Std/Tactic/Lint/Basic.lean
@@ -3,9 +3,8 @@ Copyright (c) 2020 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn, Robert Y. Lewis, Gabriel Ebner
 -/
-
 import Std.Util.TermUnsafe
-import Std.Lean.NameMapAttribute
+
 open Lean Meta
 
 namespace Std.Tactic.Lint

diff --git a/Std/Tactic/Omega/Coeffs/IntList.lean b/Std/Tactic/Omega/Coeffs/IntList.lean
@@ -1,5 +1,4 @@
 import Std.Tactic.Omega.IntList
-import Std.Tactic.Omega.MinNatAbs
 
 /-!
 # `Coeffs` as a wrapper for `IntList`

diff --git a/Std/Tactic/Omega/Constraint.lean b/Std/Tactic/Omega/Constraint.lean
@@ -3,9 +3,10 @@ Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
+import Std.Classes.Order
 import Std.Tactic.RCases
 import Std.Tactic.NormCast
-import Std.Tactic.Omega.OmegaM
+import Std.Tactic.Omega.Coeffs.IntList
 
 /-!
 A `Constraint` consists of an optional lower and upper bound (inclusive),

diff --git a/Std/Tactic/Omega/Core.lean b/Std/Tactic/Omega/Core.lean
@@ -5,7 +5,8 @@ Authors: Scott Morrison
 -/
 import Std.Tactic.Omega.OmegaM
 import Std.Tactic.Omega.Constraint
-import Std.Data.HashMap
+import Std.Tactic.Omega.MinNatAbs
+import Std.Data.HashMap.Basic
 
 open Lean (HashSet)
 

diff --git a/Std/Tactic/Relation/Symm.lean b/Std/Tactic/Relation/Symm.lean
@@ -3,6 +3,8 @@ Copyright (c) 2022 Siddhartha Gadgil. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Siddhartha Gadgil, Mario Carneiro, Scott Morrison
 -/
+import Lean.Meta.Reduce
+import Lean.Elab.Tactic.Location
 import Std.Lean.Meta.Basic
 
 /-!

diff --git a/Std/Tactic/SolveByElim.lean b/Std/Tactic/SolveByElim.lean
@@ -3,7 +3,6 @@ Copyright (c) 2021 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison, David Renshaw
 -/
-import Std.Data.Option.Basic
 import Std.Data.Sum.Basic
 import Std.Tactic.LabelAttr
 import Std.Tactic.Relation.Symm

diff --git a/Std/Util/ProofWanted.lean b/Std/Util/ProofWanted.lean
@@ -5,7 +5,6 @@ Authors: David Thrane Christiansen
 -/
 import Lean.Elab.Exception
 import Lean.Elab.Command
-import Lean.Parser
 
 
 open Lean Parser Elab Command