Trigger CI for leanprover/lean4#3718

leanprover-community · Sep 23, 2024 · 21c475d · 21c475d
2 parents b03e617 + f51886e
commit 21c475d
Showing 1 changed file with 0 additions and 7 deletions.
diff --git a/Batteries/Lean/HashSet.lean b/Batteries/Lean/HashSet.lean
@@ -59,10 +59,3 @@ def insert' (s : HashSet α) (a : α) : HashSet α × Bool :=
   let oldSize := s.size
   let s := s.insert a
   (s, s.size == oldSize)
-
-/--
-`O(n)`. Obtain a `HashSet` from an array.
--/
-@[inline]
-protected def ofArray [BEq α] [Hashable α] (as : Array α) : HashSet α :=
-  HashSet.empty.insertMany as