chore: deprecate HashSet.insert' (#949)

leanprover-community · Sep 18, 2024 · 2ce0037 · 2ce0037
1 parent 46fed98
commit 2ce0037
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Batteries/Lean/HashSet.lean b/Batteries/Lean/HashSet.lean
@@ -54,7 +54,7 @@ instance : BEq (HashSet α) where
 `O(1)` amortized. Similar to `insert`, but also returns a Boolean flag indicating whether an
 existing entry has been replaced with `a => b`.
 -/
-@[inline]
+@[inline, deprecated containsThenInsert (since := "2024-09-17")]
 def insert' (s : HashSet α) (a : α) : HashSet α × Bool :=
   let oldSize := s.size
   let s := s.insert a