feat: add HashSet.insertMany

bollu · Nov 28, 2022 · a3dfa55 · a3dfa55
1 parent 36cc7c2
commit a3dfa55
Showing 1 changed file with 7 additions and 0 deletions.
diff --git a/src/Lean/Data/HashSet.lean b/src/Lean/Data/HashSet.lean
@@ -187,3 +187,10 @@ def toArray (m : HashSet α) : Array α :=
 
 def numBuckets (m : HashSet α) : Nat :=
   m.val.buckets.val.size
+
+/-- Insert many elements into a HashSet. -/
+def insertMany [ForIn Id ρ α] (s : HashSet α) (as : ρ) : HashSet α := Id.run do
+  let mut s := s
+  for a in as do
+    s := s.insert a
+  return s