chore: deprecate Array.split in favour of identical Array.partition (#5970)

src/Init/Data/Array/Basic.lean

@@ -866,6 +866,7 @@ def zip (as : Array α) (bs : Array β) : Array (α × β) :=
 def unzip (as : Array (α × β)) : Array α × Array β :=
   as.foldl (init := (#[], #[])) fun (as, bs) (a, b) => (as.push a, bs.push b)
 
+@[deprecated partition (since := "2024-11-06")]
 def split (as : Array α) (p : α → Bool) : Array α × Array α :=
   as.foldl (init := (#[], #[])) fun (as, bs) a =>
     if p a then (as.push a, bs) else (as, bs.push a)

src/Lean/Elab/Match.lean

@@ -957,7 +957,7 @@ where
     let mut s : CollectFVars.State := {}
     for discr in discrs do
       s := collectFVars s (← instantiateMVars (← inferType discr))
-    let (indicesFVar, indicesNonFVar) := indices.split Expr.isFVar
+    let (indicesFVar, indicesNonFVar) := indices.partition Expr.isFVar
     let indicesFVar := indicesFVar.map Expr.fvarId!
     let mut toAdd := #[]
     for fvarId in s.fvarSet.toList do