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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
