From d36a34b13e88278ba18ebcd2a85bd53b57072622 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Wed, 30 Oct 2024 11:37:21 +1100
Subject: [PATCH] chore: rename List.groupBy to splitBy

---
 src/Init/Data/List/Basic.lean | 18 ++++++++++--------
 src/Init/Data/List/Impl.lean  |  2 +-
 2 files changed, 11 insertions(+), 9 deletions(-)

diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean
index d9936e220c7a..8a7631d03b11 100644
--- a/src/Init/Data/List/Basic.lean
+++ b/src/Init/Data/List/Basic.lean
@@ -45,7 +45,7 @@ The operations are organized as follow:
 * Zippers: `zipWith`, `zip`, `zipWithAll`, and `unzip`.
 * Ranges and enumeration: `range`, `iota`, `enumFrom`, and `enum`.
 * Minima and maxima: `min?` and `max?`.
-* Other functions: `intersperse`, `intercalate`, `eraseDups`, `eraseReps`, `span`, `groupBy`,
+* Other functions: `intersperse`, `intercalate`, `eraseDups`, `eraseReps`, `span`, `splitBy`,
   `removeAll`
   (currently these functions are mostly only used in meta code,
   and do not have API suitable for verification).
@@ -1639,23 +1639,23 @@ where
     | true  => loop as (a::rs)
     | false => (rs.reverse, a::as)
 
-/-! ### groupBy -/
+/-! ### splitBy -/
 
 /--
-`O(|l|)`. `groupBy R l` splits `l` into chains of elements
+`O(|l|)`. `splitBy R l` splits `l` into chains of elements
 such that adjacent elements are related by `R`.
 
-* `groupBy (·==·) [1, 1, 2, 2, 2, 3, 2] = [[1, 1], [2, 2, 2], [3], [2]]`
-* `groupBy (·<·) [1, 2, 5, 4, 5, 1, 4] = [[1, 2, 5], [4, 5], [1, 4]]`
+* `splitBy (·==·) [1, 1, 2, 2, 2, 3, 2] = [[1, 1], [2, 2, 2], [3], [2]]`
+* `splitBy (·<·) [1, 2, 5, 4, 5, 1, 4] = [[1, 2, 5], [4, 5], [1, 4]]`
 -/
-@[specialize] def groupBy (R : α → α → Bool) : List α → List (List α)
+@[specialize] def splitBy (R : α → α → Bool) : List α → List (List α)
   | []    => []
   | a::as => loop as a [] []
 where
   /--
-  The arguments of `groupBy.loop l ag g gs` represent the following:
+  The arguments of `splitBy.loop l ag g gs` represent the following:
 
-  - `l : List α` are the elements which we still need to group.
+  - `l : List α` are the elements which we still need to split.
   - `ag : α` is the previous element for which a comparison was performed.
   - `g : List α` is the group currently being assembled, in **reverse order**.
   - `gs : List (List α)` is all of the groups that have been completed, in **reverse order**.
@@ -1666,6 +1666,8 @@ where
     | false => loop as a [] ((ag::g).reverse::gs)
   | [], ag, g, gs => ((ag::g).reverse::gs).reverse
 
+@[deprecated splitBy (since := "2024-10-30"), inherit_doc splitBy] abbrev groupBy := @splitBy
+
 /-! ### removeAll -/
 
 /-- `O(|xs|)`. Computes the "set difference" of lists,
diff --git a/src/Init/Data/List/Impl.lean b/src/Init/Data/List/Impl.lean
index 782316bf7b99..9e85de85bcef 100644
--- a/src/Init/Data/List/Impl.lean
+++ b/src/Init/Data/List/Impl.lean
@@ -23,7 +23,7 @@ namespace List
 The following operations are already tail-recursive, and do not need `@[csimp]` replacements:
 `get`, `foldl`, `beq`, `isEqv`, `reverse`, `elem` (and hence `contains`), `drop`, `dropWhile`,
 `partition`, `isPrefixOf`, `isPrefixOf?`, `find?`, `findSome?`, `lookup`, `any` (and hence `or`),
-`all` (and hence `and`) , `range`, `eraseDups`, `eraseReps`, `span`, `groupBy`.
+`all` (and hence `and`) , `range`, `eraseDups`, `eraseReps`, `span`, `splitBy`.
 
 The following operations are still missing `@[csimp]` replacements:
 `concat`, `zipWithAll`.