chore: adaptations for nightly-2024-08-11 (#912)

Co-authored-by: leanprover-community-mathlib4-bot <[email protected]> Co-authored-by: Wojciech Nawrocki <[email protected]> Co-authored-by: L <[email protected]> Co-authored-by: Joachim Breitner <[email protected]> Co-authored-by: Kyle Miller <[email protected]>
leanprover-community · Aug 12, 2024 · aba8b25 · aba8b25
1 parent 4ff2a6a
commit aba8b25
Show file tree

Hide file tree

Showing 11 changed files with 15 additions and 34 deletions.
diff --git a/Batteries.lean b/Batteries.lean
@@ -35,7 +35,6 @@ import Batteries.Data.Range
 import Batteries.Data.Rat
 import Batteries.Data.String
 import Batteries.Data.Sum
-import Batteries.Data.Thunk
 import Batteries.Data.UInt
 import Batteries.Data.UnionFind
 import Batteries.Lean.AttributeExtra

diff --git a/Batteries/Data/ByteArray.lean b/Batteries/Data/ByteArray.lean
@@ -131,7 +131,7 @@ private def ofFnAux (f : Fin n → UInt8) : ByteArray := go 0 (mkEmpty n) where
 termination_by n - i
 
 @[csimp] private theorem ofFn_eq_ofFnAux : @ofFn = @ofFnAux := by
-  funext n f; ext; simp [ofFnAux, Array.ofFn, ofFnAux_data, mkEmpty]
+  funext n f; ext1; simp [ofFnAux, Array.ofFn, ofFnAux_data, mkEmpty]
 where
   ofFnAux_data {n} (f : Fin n → UInt8) (i) {acc} :
       (ofFnAux.go f i acc).data = Array.ofFn.go f i acc.data := by

diff --git a/Batteries/Data/LazyList.lean b/Batteries/Data/LazyList.lean
@@ -3,7 +3,7 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Simon Hudon
 -/
-import Batteries.Data.Thunk
+
 /-!
 # Lazy lists
 

diff --git a/Batteries/Data/Thunk.lean b/Batteries/Data/Thunk.lean
diff --git a/Batteries/Data/UnionFind/Basic.lean b/Batteries/Data/UnionFind/Basic.lean
@@ -5,6 +5,7 @@ Authors: Mario Carneiro
 -/
 import Batteries.Tactic.Lint.Misc
 import Batteries.Tactic.SeqFocus
+import Batteries.Data.Array.Lemmas
 
 namespace Batteries
 

diff --git a/Batteries/Lean/AttributeExtra.lean b/Batteries/Lean/AttributeExtra.lean
@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 import Batteries.Lean.TagAttribute
+import Std.Data.HashMap.Basic
+
 open Lean
 
 namespace Lean
@@ -75,7 +77,7 @@ structure ParametricAttributeExtra (α : Type) where
   /-- The underlying `ParametricAttribute`. -/
   attr : ParametricAttribute α
   /-- A list of pre-tagged declarations with their values. -/
-  base : HashMap Name α
+  base : Std.HashMap Name α
   deriving Inhabited
 
 /--

diff --git a/Batteries/Lean/HashMap.lean b/Batteries/Lean/HashMap.lean
@@ -4,22 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jannis Limperg
 -/
 
-import Lean.Data.HashMap
-
-namespace Lean.HashMap
+import Std.Data.HashMap.Basic
+namespace Std.HashMap
 
 variable [BEq α] [Hashable α]
 
-instance : ForIn m (HashMap α β) (α × β) where
-  forIn m init f := do
-    let mut acc := init
-    for buckets in m.val.buckets.val do
-      for d in buckets do
-        match ← f d acc with
-        | .done b => return b
-        | .yield b => acc := b
-    return acc
-
 /--
 `O(|other|)` amortized. Merge two `HashMap`s.
 The values of keys which appear in both maps are combined using the monadic function `f`.
@@ -28,7 +17,7 @@ The values of keys which appear in both maps are combined using the monadic func
 def mergeWithM {m α β} [BEq α] [Hashable α] [Monad m] (f : α → β → β → m β)
     (self other : HashMap α β) : m (HashMap α β) :=
   other.foldM (init := self) fun map k v₂ =>
-    match map.find? k with
+    match map[k]? with
     | none => return map.insert k v₂
     | some v₁ => return map.insert k (← f k v₁ v₂)
 
@@ -41,6 +30,6 @@ def mergeWith (f : α → β → β → β) (self other : HashMap α β) : HashM
   -- Implementing this function directly, rather than via `mergeWithM`, gives
   -- us less constrained universes.
   other.fold (init := self) fun map k v₂ =>
-    match map.find? k with
+    match map[k]? with
     | none => map.insert k v₂
     | some v₁ => map.insert k <| f k v₁ v₂
diff --git a/Batteries/Lean/Meta/Inaccessible.lean b/Batteries/Lean/Meta/Inaccessible.lean
@@ -15,7 +15,7 @@ later fvar with the same user name.
 def Lean.LocalContext.inaccessibleFVars (lctx : LocalContext) :
     Array LocalDecl :=
   let (result, _) :=
-    lctx.foldr (β := Array LocalDecl × HashSet Name)
+    lctx.foldr (β := Array LocalDecl × Std.HashSet Name)
       (init := (Array.mkEmpty lctx.numIndices, {}))
       fun ldecl (result, seen) =>
         if ldecl.isImplementationDetail then

diff --git a/Batteries/Linter/UnnecessarySeqFocus.lean b/Batteries/Linter/UnnecessarySeqFocus.lean
@@ -83,7 +83,7 @@ structure Entry where
   used : Bool
 
 /-- The monad for collecting used tactic syntaxes. -/
-abbrev M (ω) := StateRefT (HashMap String.Range Entry) (ST ω)
+abbrev M (ω) := StateRefT (Std.HashMap String.Range Entry) (ST ω)
 
 /-- True if this is a `<;>` node in either `tactic` or `conv` classes. -/
 @[inline] def isSeqFocus (k : SyntaxNodeKind) : Bool :=

diff --git a/Batteries/Linter/UnreachableTactic.lean b/Batteries/Linter/UnreachableTactic.lean
@@ -29,14 +29,14 @@ namespace UnreachableTactic
 def getLinterUnreachableTactic (o : Options) : Bool := getLinterValue linter.unreachableTactic o
 
 /-- The monad for collecting used tactic syntaxes. -/
-abbrev M := StateRefT (HashMap String.Range Syntax) IO
+abbrev M := StateRefT (Std.HashMap String.Range Syntax) IO
 
 /--
 A list of blacklisted syntax kinds, which are expected to have subterms that contain
 unevaluated tactics.
 -/
 initialize ignoreTacticKindsRef : IO.Ref NameHashSet ←
-  IO.mkRef <| HashSet.empty
+  IO.mkRef <| Std.HashSet.empty
     |>.insert ``Parser.Term.binderTactic
     |>.insert ``Lean.Parser.Term.dynamicQuot
     |>.insert ``Lean.Parser.Tactic.quotSeq

diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2024-08-08
+leanprover/lean4:nightly-2024-08-11