However:
You can express a property such as "takeWhile p xs ++ dropWhile p xs === xs" and it will prove it to be true for all values of p :: a -> Bool and xs :: [a], over all types a, using only the function definitions.
That is surprising, given that this property does not seem to be true for p = const undefined and xs /= [].
Tillmann
This is a very interesting observation. When Zeno does induction/case-splitting it does not consider the value _|_ as a potential inhabitant of a type. This could be a feature I might add in a later version or some option for being able to turn this behaviour on/off but thanks for spotting it. Infinite values (lazy-evaluation in general) also give Zeno a problem, since you can no longer use structure as a well-defined ordering for induction. A property such as "reverse (reverse xs) === xs" does not work for infinite lists, since you can successfully case-analyse values from "xs" but case-analysing "reverse (reverse xs)" will give an infinite loop. You could say the values are equal in some sense (maybe given infinite computation time) but they do not behave in the same way. Cheers, Will