From 078e9b6d778932430adf9ecbbf02e1025e922ce1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Violeta=20Hern=C3=A1ndez?= Date: Sun, 15 Sep 2024 23:56:44 -0600 Subject: [PATCH] doc: add documentation for `groupBy.loop` (#5349) We add some documentation explaining the auxiliary function in the definition of `groupBy`. This has been moved here from Mathlib PR [16818](https://github.com/leanprover-community/mathlib4/pull/16818) by request of @semorrison. --------- Co-authored-by: Kim Morrison --- src/Init/Data/List/Basic.lean | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean index 4bfd0225b799..07b598891829 100644 --- a/src/Init/Data/List/Basic.lean +++ b/src/Init/Data/List/Basic.lean @@ -1588,6 +1588,14 @@ such that adjacent elements are related by `R`. | [] => [] | a::as => loop as a [] [] where + /-- + The arguments of `groupBy.loop l ag g gs` represent the following: + + - `l : List α` are the elements which we still need to group. + - `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**. + -/ @[specialize] loop : List α → α → List α → List (List α) → List (List α) | a::as, ag, g, gs => match R ag a with | true => loop as a (ag::g) gs