chore: fix implicitness in HashMap.ofList (#4248)
Reported at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Typeclass.20Inference.20Failure.20on.20HashMap/near/439842209
This commit is contained in:
parent
8ca00918fb
commit
c2b8a1e618
1 changed files with 3 additions and 0 deletions
|
|
@ -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
|
||||
|
||||
/--
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue