5 Sep
2006
5 Sep
'06
2:21 p.m.
G'day all. Quoting Janis Voigtlaender <voigt@tcs.inf.tu-dresden.de>:
I find the omission of quantifications in the produced theorems problematic.
I agree. Indeed, if you look at the source code, the quantifications _are_ generated, they're just not printed. The reason is that the output was (re-)designed for use on IRC where space is at a premium. However, you're correct that sometimes they're semantically important. Fixed.
For this, you produce the following theorem:
g x = h (f x) => $map f . filter g = filter h . $map f
It now produces: filter (f . g) . $map f = $map f . filter g Cheers, Andrew Bromage