chore: fix implicitness in HashMap.ofList

leanprover · May 22, 2024 · 8b02950 · 8b02950
1 parent 2faa81d
commit 8b02950
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/src/Lean/Data/HashMap.lean b/src/Lean/Data/HashMap.lean
@@ -249,6 +249,8 @@ def toArray (m : HashMap α β) : Array (α × β) :=
 def numBuckets (m : HashMap α β) : Nat :=
   m.val.buckets.val.size
 
+variable [BEq α] [Hashable α]
+
 /-- Builds a `HashMap` from a list of key-value pairs. Values of duplicated keys are replaced by their respective last occurrences. -/
 def ofList (l : List (α × β)) : HashMap α β :=
   l.foldl (init := HashMap.empty) (fun m p => m.insert p.fst p.snd)
@@ -260,6 +262,7 @@ def ofListWith (l : List (α × β)) (f : β → β → β) : HashMap α β :=
       match m.find? p.fst with
         | none   => m.insert p.fst p.snd
         | some v => m.insert p.fst $ f v p.snd)
+
 end Lean.HashMap
 
 /--