From 8b02950a3a2ffb7bf09b1834c301b18ba3acdedd Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Wed, 22 May 2024 12:47:23 +1000
Subject: [PATCH] chore: fix implicitness in HashMap.ofList

---
 src/Lean/Data/HashMap.lean | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/Lean/Data/HashMap.lean b/src/Lean/Data/HashMap.lean
index 387629fc9465..a4016e04465b 100644
--- 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
 
 /--