Skip to content

Commit

Permalink
perf: fix linearity issue in insertIfNew (#3881)
Browse files Browse the repository at this point in the history
This fixes a linearity isssue in `insertIfNew`. As `insertIfNew` is used
in `Lean.finalizeImport` we expect this to improve performance.
  • Loading branch information
hargoniX authored Apr 11, 2024
1 parent 36f1398 commit 3ed2d9b
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/Lean/Data/HashMap.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit 3ed2d9b

Please sign in to comment.