[Haskell-cafe] Re: ANNOUNCE zeno 0.1.0

[Tillmann Rendel]

Will Sonnex wrote:
> Zeno is a fully automated inductive theorem proving tool for Haskell programs.

I tried it via the web interface, and it seems to be quite cool. Good work!

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