[Haskell-cafe] Re: ANNOUNCE zeno 0.1.0
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
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