-- The definition of the function `split` from library `List`.
split :: (a -> Bool) -> [a] -> [[a]]
split _ []     = [[]]
split p (x:xs) | p x       = [] : split p xs
               | otherwise = let sp = split p xs
                             in (x : head sp) : tail sp

-- This postcondition is useful to verify that the calls to head and split
-- are non-failing (compare package `failfree`).
split'post :: (a -> Bool) -> [a] -> [[a]] -> Bool
split'post p xs ys = not (null ys)