Skip to content

Commit

Permalink
remote unneeded implicit argument hints
Browse files Browse the repository at this point in the history
  • Loading branch information
datokrat committed Jan 10, 2025
1 parent 912a4f7 commit fd800a0
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions src/Std/Data/DHashMap/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -253,11 +253,11 @@ Modifies in place the value associated with a given key.
This function ensures that the value is used linearly.
-/
@[inline] def modify [LawfulBEq α] (m : DHashMap α β) (a : α) (f : β a → β a) : DHashMap α β :=
⟨Raw₀.modify (α := α) ⟨m.1, m.2.size_buckets_pos⟩ a f, Raw.WF.modify₀ m.2
⟨Raw₀.modify ⟨m.1, m.2.size_buckets_pos⟩ a f, Raw.WF.modify₀ m.2

@[inline, inherit_doc DHashMap.modify] def Const.modify {β : Type v} (m : DHashMap α (fun _ => β))
(a : α) (f : β → β) : DHashMap α (fun _ => β) :=
⟨Raw₀.Const.modify (α := α) ⟨m.1, m.2.size_buckets_pos⟩ a f, Raw.WF.constModify₀ m.2
⟨Raw₀.Const.modify ⟨m.1, m.2.size_buckets_pos⟩ a f, Raw.WF.constModify₀ m.2

/--
Modifies in place the value associated with a given key,
Expand Down

0 comments on commit fd800a0

Please sign in to comment.