Hi Actually, you can go slightly better: words s = case dropWhile isSpace s of [] -> [] (s:ss) -> (s:w) : drop1 sss where (w, sss) = break isSpace ss drop1 [] = [] drop1 (x:xs) = words xs Although a good optimising compiler may make this last leap all on its own.
To really convince yourself and everyone else you could compare it against the spec, for both total and partial values.
I'm pretty convinced that I applied reasoning rules at each stage. If you have a proof, testing is irrelevant :-) I've already modified the Yhc base library with this optimisation, and done some basic testing, and nothing broke. Thanks Neil