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 2d42d0b commit a0a7be3Copy full SHA for a0a7be3
src/Std/Data/HashSet/Raw.lean
@@ -264,7 +264,7 @@ section Unverified
264
265
@[inline, inherit_doc HashMap.Raw.partition] def partition [BEq α] [Hashable α] (f : α → Bool)
266
(m : Raw α) : Raw α × Raw α :=
267
- let ⟨l, r⟩ := m.inner.partition f
+ let ⟨l, r⟩ := m.inner.partition (fun a _ => f a)
268
⟨⟨l⟩, ⟨r⟩⟩
269
270
/-! We currently do not provide lemmas for the functions below. -/
0 commit comments