From 63c1c38b123b0741b7b7fd56fb8510f95bfd0e55 Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Thu, 3 Oct 2024 14:21:23 +0200
Subject: [PATCH] fix: botched merge
---
Batteries/Data/HashMap/WF.lean | 22 ++++++++++------------
1 file changed, 10 insertions(+), 12 deletions(-)
diff --git a/Batteries/Data/HashMap/WF.lean b/Batteries/Data/HashMap/WF.lean
index 11b68de28d..c95e3ad133 100644
--- a/Batteries/Data/HashMap/WF.lean
+++ b/Batteries/Data/HashMap/WF.lean
@@ -387,15 +387,13 @@ variable {_ : BEq α} {_ : Hashable α}
@[inline] def mapVal (f : α → β → γ) (self : HashMap α β) : HashMap α γ :=
⟨self.1.mapVal f, self.2.mapVal⟩
--- Temporarily removed on lean-pr-testing-5403.
-
--- /--
--- Applies `f` to each key-value pair `a, b` in the map. If it returns `some c` then
--- `a, c` is pushed into the new map; else the key is removed from the map.
--- -/
--- @[inline] def filterMap (f : α → β → Option γ) (self : HashMap α β) : HashMap α γ :=
--- ⟨self.1.filterMap f, self.2.filterMap⟩
-
--- /-- Constructs a map with the set of all pairs `a, b` such that `f` returns true. -/
--- @[inline] def filter (f : α → β → Bool) (self : HashMap α β) : HashMap α β :=
--- self.filterMap fun a b => bif f a b then some b else none
+/--
+Applies `f` to each key-value pair `a, b` in the map. If it returns `some c` then
+`a, c` is pushed into the new map; else the key is removed from the map.
+-/
+@[inline] def filterMap (f : α → β → Option γ) (self : HashMap α β) : HashMap α γ :=
+ ⟨self.1.filterMap f, self.2.filterMap⟩
+
+/-- Constructs a map with the set of all pairs `a, b` such that `f` returns true. -/
+@[inline] def filter (f : α → β → Bool) (self : HashMap α β) : HashMap α β :=
+ self.filterMap fun a b => bif f a b then some b else none