From ec93feb5a94896b9ff3e96adcda5ec873631d887 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Fri, 12 Apr 2024 04:28:13 -0400 Subject: [PATCH] fix: linearity in HashMap.erase port of leanprover/lean4#3887 to Std --- Std/Data/HashMap/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Std/Data/HashMap/Basic.lean b/Std/Data/HashMap/Basic.lean index 247db447ef..b591ac480a 100644 --- a/Std/Data/HashMap/Basic.lean +++ b/Std/Data/HashMap/Basic.lean @@ -179,7 +179,7 @@ def erase [BEq α] [Hashable α] (m : Imp α β) (a : α) : Imp α β := let ⟨size, buckets⟩ := m let ⟨i, h⟩ := mkIdx buckets.2 (hash a |>.toUSize) let bkt := buckets.1[i] - bif bkt.contains a then ⟨size - 1, buckets.update i (bkt.erase a) h⟩ else m + bif bkt.contains a then ⟨size - 1, buckets.update i (bkt.erase a) h⟩ else ⟨size, buckets⟩ /-- Map a function over the values in the map. -/ @[inline] def mapVal (f : α → β → γ) (self : Imp α β) : Imp α γ :=