edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-11-24 04:43:25 +03:00
Code Issues Projects Releases Wiki Activity

Fix comment.

Browse Source
This commit is contained in:
Matus Tejiscak 2020-03-29 19:50:43 +02:00
parent 9154a9b02b
commit fcdfa8e191
1 changed files with 3 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
libs/base/Data/List.idr
View File

@ -392,9 +392,10 @@ sortBy cmp xs = let (x, y) = split xs in
splitRec : List b -> List a -> (List a -> List a) -> (List a, List a)
splitRec (_::_::xs) (y::ys) zs = splitRec xs ys (zs . ((::) y))
splitRec _ ys zs = (ys, zs [])
-- In the above base-case clause, we put `ys` first to get a stable sort.
-- In the above base-case clause, we put `ys` on the LHS to get a stable sort.
-- This is because `mergeBy` prefers taking elements from its RHS operand
-- if both heads are equal.
-- if both heads are equal, and all elements in `zs []` precede all elements of `ys`
-- in the original list.
split : List a -> (List a, List a)
split xs = splitRec xs xs id