From 5d2bd1e2e4ab4212f347c08cd7464b673f9e1c39 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 6 Nov 2024 11:37:33 +1100 Subject: [PATCH] chore: deprecate Array.split in favour of identical Array.partition (#5970) --- src/Init/Data/Array/Basic.lean | 1 + src/Lean/Elab/Match.lean | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean index 662f6cfd10..3e924e1b3c 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) diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean index d2e7a02c4d..36cedb2b4a 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