From 77869a644746ab9a63a10e3c369aafa627fa899b Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 6 Nov 2024 09:33:27 +1100 Subject: [PATCH 1/2] chore: deprecate Array.split in favour of identical Array.partition --- src/Init/Data/Array/Basic.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean index 662f6cfd100d..3e924e1b3c1c 100644 --- a/src/Init/Data/Array/Basic.lean +++ b/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) From d8aeda782356958dbd37076cc3224cafb528c9f3 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 6 Nov 2024 10:11:32 +1100 Subject: [PATCH 2/2] deprecation --- src/Lean/Elab/Match.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean index d2e7a02c4db2..36cedb2b4ae3 100644 --- a/src/Lean/Elab/Match.lean +++ b/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