merge main

leanprover-community · Aug 12, 2024 · 4ff2a6a · 4ff2a6a
2 parents 2fae043 + ad26fe1
commit 4ff2a6a
Show file tree

Hide file tree

Showing 30 changed files with 22 additions and 38 deletions.
diff --git a/Batteries/CodeAction/Attr.lean b/Batteries/CodeAction/Attr.lean
@@ -3,7 +3,7 @@ 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.Server.CodeActions
+import Lean.Server.CodeActions.Basic
 
 /-!
 # Initial setup for code action attributes

diff --git a/Batteries/CodeAction/Deprecated.lean b/Batteries/CodeAction/Deprecated.lean
@@ -5,7 +5,6 @@ Authors: Mario Carneiro
 -/
 import Lean.Server.CodeActions
 import Batteries.CodeAction.Basic
-import Batteries.Lean.Position
 
 /-!
 # Code action for @[deprecated] replacements

diff --git a/Batteries/Data/ByteArray.lean b/Batteries/Data/ByteArray.lean
@@ -3,7 +3,6 @@ Copyright (c) 2023 François G. Dorais. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: François G. Dorais
 -/
-import Batteries.Data.Array.Lemmas
 
 namespace ByteArray
 

diff --git a/Batteries/Data/HashMap/Lemmas.lean b/Batteries/Data/HashMap/Lemmas.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import Batteries.Data.HashMap.Basic
-import Batteries.Data.Array.Lemmas
 
 /-!
 # Lemmas for `Batteries.HashMap`

diff --git a/Batteries/Data/HashMap/WF.lean b/Batteries/Data/HashMap/WF.lean
@@ -3,9 +3,10 @@ Copyright (c) 2022 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
+import Batteries.Tactic.SeqFocus
 import Batteries.Data.HashMap.Basic
-import Batteries.Data.Array.Lemmas
 import Batteries.Data.Nat.Lemmas
+import Batteries.Data.List.Lemmas
 
 namespace Batteries.HashMap
 namespace Imp

diff --git a/Batteries/Data/List/Pairwise.lean b/Batteries/Data/List/Pairwise.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, James Gallicchio
 -/
 import Batteries.Data.List.Count
-import Batteries.Data.Fin.Lemmas
 
 /-!
 # Pairwise relations on a list

diff --git a/Batteries/Data/Rat/Basic.lean b/Batteries/Data/Rat/Basic.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 import Batteries.Data.Nat.Gcd
-import Batteries.Data.Int.DivMod
 import Batteries.Lean.Float
 
 /-! # Basics for the Rational Numbers -/

diff --git a/Batteries/Data/String/Lemmas.lean b/Batteries/Data/String/Lemmas.lean
@@ -8,7 +8,6 @@ import Batteries.Data.List.Lemmas
 import Batteries.Data.String.Basic
 import Batteries.Tactic.Lint.Misc
 import Batteries.Tactic.SeqFocus
-import Batteries.Tactic.SqueezeScope
 
 namespace String
 

diff --git a/Batteries/Data/UnionFind/Basic.lean b/Batteries/Data/UnionFind/Basic.lean
@@ -3,8 +3,8 @@ Copyright (c) 2021 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
-import Batteries.Data.Array.Lemmas
 import Batteries.Tactic.Lint.Misc
+import Batteries.Tactic.SeqFocus
 
 namespace Batteries
 

diff --git a/Batteries/Lean/Meta/AssertHypotheses.lean b/Batteries/Lean/Meta/AssertHypotheses.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jannis Limperg
 -/
 
-import Batteries.Lean.Meta.Basic
+import Lean.Meta.Tactic.Assert
 
 open Lean Lean.Meta
 

diff --git a/Batteries/Lean/Meta/Basic.lean b/Batteries/Lean/Meta/Basic.lean
@@ -3,9 +3,7 @@ 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.Elab.Term
-import Lean.Meta.Tactic.Apply
-import Lean.Meta.Tactic.Replace
+import Lean.Meta.Tactic.Intro
 
 open Lean Lean.Meta
 

diff --git a/Batteries/Lean/Meta/Clear.lean b/Batteries/Lean/Meta/Clear.lean
@@ -5,6 +5,7 @@ Authors: Jannis Limperg
 -/
 
 import Batteries.Lean.Meta.Basic
+import Lean.Meta.Tactic.Clear
 
 open Lean Lean.Meta
 

diff --git a/Batteries/Lean/Meta/Inaccessible.lean b/Batteries/Lean/Meta/Inaccessible.lean
@@ -3,7 +3,7 @@ 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
+import Lean.Meta.Basic
 
 open Lean Lean.Meta Std
 

diff --git a/Batteries/Lean/Position.lean b/Batteries/Lean/Position.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 import Lean.Syntax
-import Lean.Meta.Tactic.TryThis
 import Lean.Data.Lsp.Utf16
 
 /-- Gets the LSP range of syntax `stx`. -/

diff --git a/Batteries/Lean/System/IO.lean b/Batteries/Lean/System/IO.lean
@@ -3,7 +3,6 @@ Copyright (c) 2023 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-import Batteries.Data.List.Lemmas
 
 /-!
 # Functions for manipulating a list of tasks

diff --git a/Batteries/Logic.lean b/Batteries/Logic.lean
@@ -3,9 +3,7 @@ Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Jeremy Avigad, Floris van Doorn, Mario Carneiro
 -/
-import Batteries.Tactic.Init
 import Batteries.Tactic.Alias
-import Batteries.Tactic.Lint.Misc
 
 instance {f : α → β} [DecidablePred p] : DecidablePred (p ∘ f) :=
   inferInstanceAs <| DecidablePred fun x => p (f x)

diff --git a/Batteries/StdDeprecations.lean b/Batteries/StdDeprecations.lean
@@ -4,12 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
 import Batteries.Tactic.Alias
-import Batteries.Data.HashMap
 import Batteries.Data.DList
 import Batteries.Data.PairingHeap
-import Batteries.Data.RBMap
-import Batteries.Data.BinomialHeap
-import Batteries.Data.UnionFind
+import Batteries.Data.BinomialHeap.Basic
+import Batteries.Data.HashMap.Basic
+import Batteries.Data.RBMap.Basic
+import Batteries.Data.UnionFind.Basic
 
 /-!
 # We set up deprecations for identifiers formerly in the `Std` namespace.

diff --git a/Batteries/Tactic/Case.lean b/Batteries/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.Conv.Pattern
+import Lean.Elab.Tactic.BuiltinTactic
 
 /-!
 # Extensions to the `case` tactic

diff --git a/Batteries/Tactic/Classical.lean b/Batteries/Tactic/Classical.lean
@@ -3,7 +3,7 @@ Copyright (c) 2021 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
-import Lean.Elab.ElabRules
+import Lean.Elab.Tactic.Basic
 
 /-! # `classical` tactic -/
 

diff --git a/Batteries/Tactic/Init.lean b/Batteries/Tactic/Init.lean
@@ -3,16 +3,14 @@ Copyright (c) 2021 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
-import Batteries.Lean.Meta.Basic
-import Lean.Elab.Command
-import Lean.Elab.Tactic.BuiltinTactic
+import Lean.Elab.Tactic.ElabTerm
 
 /-!
 # Simple tactics that are used throughout Batteries.
 -/
 
 namespace Batteries.Tactic
-open Lean Parser.Tactic Elab Command Elab.Tactic Meta
+open Lean Parser.Tactic Elab Elab.Tactic Meta
 
 /--
 `_` in tactic position acts like the `done` tactic: it fails and gives the list

diff --git a/Batteries/Tactic/NoMatch.lean b/Batteries/Tactic/NoMatch.lean
@@ -3,8 +3,8 @@ Copyright (c) 2021 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
-import Lean.Elab.ElabRules
 import Lean.DocString
+import Lean.Elab.Tactic.Basic
 
 /-!
 Deprecation warnings for `match ⋯ with.`, `fun.`, `λ.`, and `intro.`.

diff --git a/Batteries/Tactic/PrintDependents.lean b/Batteries/Tactic/PrintDependents.lean
@@ -5,7 +5,6 @@ Authors: Mario Carneiro
 -/
 import Lean.Elab.Command
 import Lean.Util.FoldConsts
-import Batteries.Lean.Delaborator
 
 /-!
 # `#print dependents` command

diff --git a/Batteries/Tactic/PrintPrefix.lean b/Batteries/Tactic/PrintPrefix.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Shing Tak Lam, Daniel Selsam, Mario Carneiro
 -/
 import Batteries.Lean.Util.EnvSearch
-import Batteries.Lean.Delaborator
 import Lean.Elab.Tactic.Config
 
 namespace Batteries.Tactic

diff --git a/Batteries/Tactic/SeqFocus.lean b/Batteries/Tactic/SeqFocus.lean
@@ -3,7 +3,7 @@ Copyright (c) 2022 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad
 -/
-import Lean.Elab.ElabRules
+import Lean.Elab.Tactic.Basic
 
 open Lean Elab Meta Tactic
 

diff --git a/Batteries/Tactic/ShowUnused.lean b/Batteries/Tactic/ShowUnused.lean
@@ -5,7 +5,6 @@ Authors: Mario Carneiro
 -/
 import Lean.Util.FoldConsts
 import Lean.Linter.UnusedVariables
-import Batteries.Lean.Delaborator
 
 /-!
 # The `#show_unused` command

diff --git a/Batteries/Tactic/Unreachable.lean b/Batteries/Tactic/Unreachable.lean
@@ -3,7 +3,7 @@ Copyright (c) 2021 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
-import Lean.Elab.ElabRules
+import Lean.Elab.Tactic.Basic
 
 namespace Batteries.Tactic
 

diff --git a/Batteries/Util/Cache.lean b/Batteries/Util/Cache.lean
@@ -3,7 +3,7 @@ Copyright (c) 2021 Gabriel Ebner. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner
 -/
-import Batteries.Lean.Meta.DiscrTree
+import Lean.Meta.DiscrTree
 
 /-!
 # Once-per-file cache for tactics

diff --git a/Batteries/Util/ExtendedBinder.lean b/Batteries/Util/ExtendedBinder.lean
@@ -3,8 +3,6 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner
 -/
-import Lean.Elab.MacroArgUtil
-import Lean.Linter.MissingDocs
 
 /-!
 Defines an extended binder syntax supporting `∀ ε > 0, ...` etc.

diff --git a/Batteries/Util/LibraryNote.lean b/Batteries/Util/LibraryNote.lean
@@ -3,7 +3,7 @@ Copyright (c) 2022 Gabriel Ebner. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner
 -/
-import Lean.Elab.ElabRules
+import Lean.Elab.Command
 
 /-!
 # Define the `library_note` command.

diff --git a/test/MLList.lean b/test/MLList.lean
@@ -1,4 +1,5 @@
 import Batteries.Data.MLList.IO
+import Batteries.Data.List.Basic
 
 set_option linter.missingDocs false