G'day all.
Quoting Janis Voigtlaender <[EMAIL PROTECTED]>:
> 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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
