perf: fix linearity issue in insertIfNew

2026-03-18 10:54:09 +00:00 · 2024-04-11 14:34:17 +02:00
1 changed files with 1 additions and 1 deletions
--- 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