feat: HashSet.Raw.all/any

src/Std/Data/HashSet/Raw.lean

@@ -188,6 +188,18 @@ instance {m : Type v → Type v} : ForM m (Raw α) α where
 instance {m : Type v → Type v} : ForIn m (Raw α) α where
   forIn m init f := m.forIn f init
 
+/-- Check if all elements satisfy the predicate, short-circuiting if a predicate fails. -/
+@[inline] def all (m : Raw α) (p : α → Bool) : Bool := Id.run do
+  for a in m do
+    if ¬ p a then return false
+  return true
+
+/-- Check if any element satisfies the predicate, short-circuiting if a predicate succeeds. -/
+@[inline] def any (m : Raw α) (p : α → Bool) : Bool := Id.run do
+  for a in m do
+    if p a then return true
+  return false
+
 /-- Transforms the hash set into a list of elements in some order. -/
 @[inline] def toList (m : Raw α) : List α :=
   m.inner.keys

tests/lean/run/hashmap.lean

@@ -374,6 +374,22 @@ def addKeyToState (k : Nat) : StateM Nat PUnit := do
     ans := k :: ans
   return ans
 
+/-- info: true -/
+#guard_msgs in
+#eval m.any fun x => x > 4
+
+/-- info: false -/
+#guard_msgs in
+#eval m.any fun x => x = 0
+
+/-- info: true -/
+#guard_msgs in
+#eval m.all fun x => x < 2^30
+
+/-- info: false -/
+#guard_msgs in
+#eval m.all fun x => x > 4
+
 /-- info: [1000000000, 2, 1] -/
 #guard_msgs in
 #eval m.toList