[Haskell-cafe] Re: ANNOUNCE zeno 0.1.0

Tillmann Rendel rendel at Mathematik.Uni-Marburg.de
Sat Nov 13 05:39:04 EST 2010

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!

> 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 /= [].


More information about the Haskell-Cafe mailing list