chore: move panicWith out of UnionFind (#983)

Batteries.lean

@@ -97,6 +97,7 @@ import Batteries.Test.Internal.DummyLabelAttr
 import Batteries.Util.Cache
 import Batteries.Util.ExtendedBinder
 import Batteries.Util.LibraryNote
+import Batteries.Util.Panic
 import Batteries.Util.Pickle
 import Batteries.Util.ProofWanted
 import Batteries.WF

Batteries/Data/UnionFind/Basic.lean

@@ -3,10 +3,15 @@ Copyright (c) 2021 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
+import Batteries.Tactic.Alias
 import Batteries.Tactic.Lint.Misc
 import Batteries.Tactic.SeqFocus
+import Batteries.Util.Panic
 import Batteries.Data.Array.Lemmas
 
+@[deprecated (since := "2024-10-05")]
+protected alias Batteries.UnionFind.panicWith := Batteries.panicWith
+
 namespace Batteries
 
 /-- Union-find node type -/
@@ -18,11 +23,6 @@ structure UFNode where
 
 namespace UnionFind
 
-/-- Panic with return value -/
-def panicWith (v : α) (msg : String) : α := @panic α ⟨v⟩ msg
-
-@[simp] theorem panicWith_eq (v : α) (msg) : panicWith v msg = v := rfl
-
 /-- Parent of a union-find node, defaults to self when the node is a root -/
 def parentD (arr : Array UFNode) (i : Nat) : Nat :=
   if h : i < arr.size then (arr.get ⟨i, h⟩).parent else i

Batteries/Util/Panic.lean

@@ -0,0 +1,12 @@
+/-
+Copyright (c) 2024 François G. Dorais. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: François G. Dorais
+-/
+
+namespace Batteries
+
+/-- Panic with a specific default value `v`. -/
+def panicWith (v : α) (msg : String) : α := @panic α ⟨v⟩ msg
+
+@[simp] theorem panicWith_eq (v : α) (msg) : panicWith v msg = v := rfl