idris-lang/Idris-dev — pull request #1220 by canndrew (2014-05-11 13:21:30+00:00)
Title: Fix List.split

This commit makes List.split behave a bit more sane and elegantly.
Currently split has the following behaviour:

0: split (== ':") "foo" -> ["foo"]
1: split (== ':") ":foo" -> ["", "foo"]
2: split (== ':") "foo:" -> ["foo"] (!!)

3: split (== ':') ":foo:foo" -> ["", "foo", "foo"]
4: split (== ':') ":foo" -> ["", "foo"]
5: split (== ':') "" -> [] (!!)

Cases 3 and 5 are the problematic ones. I would think they would result
in ["foo", ""] and [""] respectively. This patch gives split this
behaviour, it also gives split the nice property that the length of
(split ':' str) is (1 + the number of colons in str)

I've looked at the uses of split in the prelude and none of them seem to
be effected by this change.