We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent b57c16a commit 2d42d0bCopy full SHA for 2d42d0b
src/Std/Data/HashMap/Raw.lean
@@ -248,6 +248,8 @@ instance [BEq α] [Hashable α] : Union (Raw α β) := ⟨union⟩
248
249
instance [BEq α] [Hashable α] : Inter (Raw α β) := ⟨inter⟩
250
251
+instance [BEq α] [Hashable α] : SDiff (Raw α β) := ⟨diff⟩
252
+
253
@[inline, inherit_doc DHashMap.Raw.filterMap] def filterMap {γ : Type w} (f : α → β → Option γ)
254
(m : Raw α β) : Raw α γ :=
255
⟨m.inner.filterMap f⟩
0 commit comments