doc: add documentation for groupBy.loop (leanprover#5349)

We add some documentation explaining the auxiliary function in the
definition of `groupBy`. This has been moved here from Mathlib PR
[16818](leanprover-community/mathlib4#16818) by
request of @semorrison.

---------

Co-authored-by: Kim Morrison <kim@tqft.net>

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