chore: fix more Std -> Batteries (#887)

Co-authored-by: Matthew Robert Ballard <100034030+mattrobball@users.noreply.github.com>
Co-authored-by: Matthew Ballard <matt@mrb.email>

Batteries/CodeAction/Attr.lean

@@ -14,7 +14,7 @@ import Lean.Server.CodeActions.Basic
 * Attribute `@[tactic_code_action]` collects code actions which will be called
   on each occurrence of a tactic.
 -/
-namespace Std.CodeAction
+namespace Batteries.CodeAction
 
 open Lean Elab Server Lsp RequestM Snapshots
 

Batteries/CodeAction/Basic.lean

@@ -19,7 +19,7 @@ on each occurrence of a hole (`_`, `?_` or `sorry`).
 attempt to use this code action provider when browsing the `Batteries.CodeAction.Hole.Attr` file
 itself.)
 -/
-namespace Std.CodeAction
+namespace Batteries.CodeAction
 
 open Lean Elab Server RequestM CodeAction
 

Batteries/CodeAction/Deprecated.lean

@@ -14,7 +14,9 @@ This is an opt-in mechanism for making machine-applicable `@[deprecated]` defini
 whenever the deprecation lint also fires, allowing the user to replace the usage of the deprecated
 constant.
 -/
-namespace Std
+
+namespace Batteries
+
 open Lean Elab Server Lsp RequestM CodeAction
 
 /-- An environment extension for identifying `@[deprecated]` definitions which can be auto-fixed -/

Batteries/CodeAction/Misc.lean

@@ -15,7 +15,7 @@ import Lean.Server.CodeActions.Provider
 
 This declares some basic tactic code actions, using the `@[tactic_code_action]` API.
 -/
-namespace Std.CodeAction
+namespace Batteries.CodeAction
 
 open Lean Meta Elab Server RequestM CodeAction
 

Batteries/Tactic/Alias.lean

@@ -19,7 +19,7 @@ an iff theorem.
 
 namespace Batteries.Tactic.Alias
 
-open Lean Elab Parser.Command Std
+open Lean Elab Parser.Command
 
 /-- An alias can be in one of three forms -/
 inductive AliasInfo where

Batteries/Tactic/Lint/Basic.lean

@@ -9,7 +9,7 @@ import Lean.Elab.Exception
 
 open Lean Meta
 
-namespace Std.Tactic.Lint
+namespace Batteries.Tactic.Lint
 
 /-!
 # Basic linter types and attributes

Batteries/Tactic/Lint/Frontend.lean

@@ -39,7 +39,7 @@ You can append `only name1 name2 ...` to any command to run a subset of linters,
 
 You can add custom linters by defining a term of type `Linter` with the
 `@[env_linter]` attribute.
-A linter defined with the name `Std.Tactic.Lint.myNewCheck` can be run with `#lint myNewCheck`
+A linter defined with the name `Batteries.Tactic.Lint.myNewCheck` can be run with `#lint myNewCheck`
 or `#lint only myNewCheck`.
 If you add the attribute `@[env_linter disabled]` to `linter.myNewCheck` it will be
 registered, but not run by default.
@@ -52,8 +52,8 @@ omits it from only the specified linter checks.
 sanity check, lint, cleanup, command, tactic
 -/
 
-namespace Std.Tactic.Lint
-open Lean Std
+namespace Batteries.Tactic.Lint
+open Lean
 
 /-- Verbosity for the linter output. -/
 inductive LintVerbosity
@@ -97,7 +97,7 @@ Runs all the specified linters on all the specified declarations in parallel,
 producing a list of results.
 -/
 def lintCore (decls : Array Name) (linters : Array NamedLinter) :
-    CoreM (Array (NamedLinter × HashMap Name MessageData)) := do
+    CoreM (Array (NamedLinter × Std.HashMap Name MessageData)) := do
   let env ← getEnv
   let options ← getOptions -- TODO: sanitize options?
 
@@ -114,15 +114,15 @@ def lintCore (decls : Array Name) (linters : Array NamedLinter) :
           | Except.error err => pure m!"LINTER FAILED:\n{err.toMessageData}"
 
   tasks.mapM fun (linter, decls) => do
-    let mut msgs : HashMap Name MessageData := {}
+    let mut msgs : Std.HashMap Name MessageData := {}
     for (declName, msg?) in decls do
       if let some msg := msg?.get then
         msgs := msgs.insert declName msg
     pure (linter, msgs)
 
 /-- Sorts a map with declaration keys as names by line number. -/
-def sortResults (results : HashMap Name α) : CoreM <| Array (Name × α) := do
-  let mut key : HashMap Name Nat := {}
+def sortResults (results : Std.HashMap Name α) : CoreM <| Array (Name × α) := do
+  let mut key : Std.HashMap Name Nat := {}
   for (n, _) in results.toArray do
     if let some range ← findDeclarationRanges? n then
       key := key.insert n <| range.range.pos.line
@@ -140,7 +140,7 @@ def printWarning (declName : Name) (warning : MessageData) (useErrorFormat : Boo
   addMessageContextPartial m!"#check {← mkConstWithLevelParams declName} /- {warning} -/"
 
 /-- Formats a map of linter warnings using `print_warning`, sorted by line number. -/
-def printWarnings (results : HashMap Name MessageData) (filePath : System.FilePath := default)
+def printWarnings (results : Std.HashMap Name MessageData) (filePath : System.FilePath := default)
     (useErrorFormat : Bool := false) : CoreM MessageData := do
   (MessageData.joinSep ·.toList Format.line) <$>
     (← sortResults results).mapM fun (declName, warning) =>
@@ -150,10 +150,10 @@ def printWarnings (results : HashMap Name MessageData) (filePath : System.FilePa
 Formats a map of linter warnings grouped by filename with `-- filename` comments.
 The first `drop_fn_chars` characters are stripped from the filename.
 -/
-def groupedByFilename (results : HashMap Name MessageData) (useErrorFormat : Bool := false) :
+def groupedByFilename (results : Std.HashMap Name MessageData) (useErrorFormat : Bool := false) :
     CoreM MessageData := do
   let sp ← if useErrorFormat then initSrcSearchPath ["."] else pure {}
-  let grouped : HashMap Name (System.FilePath × HashMap Name MessageData) ←
+  let grouped : Std.HashMap Name (System.FilePath × Std.HashMap Name MessageData) ←
     results.foldM (init := {}) fun grouped declName msg => do
       let mod ← findModuleOf? declName
       let mod := mod.getD (← getEnv).mainModule
@@ -174,7 +174,7 @@ def groupedByFilename (results : HashMap Name MessageData) (useErrorFormat : Boo
 Formats the linter results as Lean code with comments and `#check` commands.
 -/
 def formatLinterResults
-    (results : Array (NamedLinter × HashMap Name MessageData))
+    (results : Array (NamedLinter × Std.HashMap Name MessageData))
     (decls : Array Name)
     (groupByFilename : Bool)
     (whereDesc : String) (runSlowLinters : Bool)

Batteries/Tactic/Lint/Misc.lean

@@ -14,7 +14,7 @@ import Batteries.Tactic.Lint.Basic
 
 open Lean Meta Std
 
-namespace Std.Tactic.Lint
+namespace Batteries.Tactic.Lint
 
 /-!
 # Various linters
@@ -143,7 +143,7 @@ In pseudo-mathematical form, this returns `{{p : parameter | p ∈ u} | (u : lev
 FIXME: We use `Array Name` instead of `HashSet Name`, since `HashSet` does not have an equality
 instance. It will ignore `nm₀.proof_i` declarations.
 -/
-private def univParamsGrouped (e : Expr) (nm₀ : Name) : HashSet (Array Name) :=
+private def univParamsGrouped (e : Expr) (nm₀ : Name) : Std.HashSet (Array Name) :=
   runST fun σ => do
     let res ← ST.mkRef (σ := σ) {}
     e.forEach fun

Batteries/Tactic/Lint/Simp.lean

@@ -9,7 +9,7 @@ import Batteries.Tactic.OpenPrivate
 import Batteries.Util.LibraryNote
 open Lean Meta
 
-namespace Std.Tactic.Lint
+namespace Batteries.Tactic.Lint
 
 /-!
 # Linter for simplification lemmas
@@ -86,8 +86,6 @@ where
   | Trie.node vs children =>
     children.foldl (init := arr ++ vs) fun arr (_, child) => trieElements arr child
 
-open Std
-
 /-- Add message `msg` to any errors thrown inside `k`. -/
 def decorateError (msg : MessageData) (k : MetaM α) : MetaM α := do
   try k catch e => throw (.error e.getRef m!"{msg}\n{e.toMessageData}")

Batteries/Tactic/Lint/TypeClass.lean

@@ -6,7 +6,7 @@ Authors: Gabriel Ebner
 import Lean.Meta.Instances
 import Batteries.Tactic.Lint.Basic
 
-namespace Std.Tactic.Lint
+namespace Batteries.Tactic.Lint
 open Lean Meta
 
 /--

scripts/runLinter.lean

@@ -2,7 +2,7 @@ import Lean.Util.SearchPath
 import Batteries.Tactic.Lint
 import Batteries.Data.Array.Basic
 
-open Lean Core Elab Command Std.Tactic.Lint
+open Lean Core Elab Command Batteries.Tactic.Lint
 open System (FilePath)
 
 /-- The list of `nolints` pulled from the `nolints.json` file -/

test/lintTC.lean

@@ -1,7 +1,7 @@
 import Batteries.Tactic.Lint.TypeClass
 import Lean.Elab.Command
 
-open Std.Tactic.Lint
+open Batteries.Tactic.Lint
 
 namespace A
 

test/lintsimp.lean

@@ -1,6 +1,6 @@
 import Batteries.Tactic.Lint
 
-open Std.Tactic.Lint
+open Batteries.Tactic.Lint
 set_option linter.missingDocs false
 
 def f : Nat := 0