13 Nov
2010
13 Nov
'10
5:39 a.m.
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