@@ -1686,17 +1686,17 @@ where
1686
1686
`O(|l|)`. `splitBy R l` splits `l` into chains of elements
1687
1687
such that adjacent elements are related by `R`.
1688
1688
1689
- * `groupBy (·==·) [1, 1, 2, 2, 2, 3, 2] = [[1, 1], [2, 2, 2], [3], [2]]`
1690
- * `groupBy (·<·) [1, 2, 5, 4, 5, 1, 4] = [[1, 2, 5], [4, 5], [1, 4]]`
1689
+ * `splitBy (·==·) [1, 1, 2, 2, 2, 3, 2] = [[1, 1], [2, 2, 2], [3], [2]]`
1690
+ * `splitBy (·<·) [1, 2, 5, 4, 5, 1, 4] = [[1, 2, 5], [4, 5], [1, 4]]`
1691
1691
-/
1692
- @[specialize] def groupBy (R : α → α → Bool) : List α → List (List α)
1692
+ @[specialize] def splitBy (R : α → α → Bool) : List α → List (List α)
1693
1693
| [] => []
1694
1694
| a::as => loop as a [] []
1695
1695
where
1696
1696
/--
1697
- The arguments of `groupBy .loop l ag g gs` represent the following:
1697
+ The arguments of `splitBy .loop l ag g gs` represent the following:
1698
1698
1699
- - `l : List α` are the elements which we still need to group .
1699
+ - `l : List α` are the elements which we still need to split .
1700
1700
- `ag : α` is the previous element for which a comparison was performed.
1701
1701
- `g : List α` is the group currently being assembled, in **reverse order** .
1702
1702
- `gs : List (List α)` is all of the groups that have been completed, in **reverse order** .
0 commit comments