perf: fix linearity issue in insertIfNew

leanprover · Apr 11, 2024 · faab75b · faab75b
1 parent 68e3982
commit faab75b
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/Lean/Data/HashMap.lean b/src/Lean/Data/HashMap.lean
@@ -122,7 +122,7 @@ def expand [Hashable α] (size : Nat) (buckets : HashMapBucket α β) : HashMapI
     let ⟨i, h⟩ := mkIdx (hash a) buckets.property
     let bkt    := buckets.val[i]
     if let some b := bkt.find? a then
-      (m, some b)
+      (⟨size, buckets⟩, some b)
     else
       let size'    := size + 1
       let buckets' := buckets.update i (AssocList.cons a b bkt) h