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
[EMAIL PROTECTED] wrote:
G'day all.
Quoting Donald Bruce Stewart [EMAIL PROTECTED]:
Get some free theorems:
lambdabot free f :: (b - b) - [b] - [b]
f . g = h . f = map f . f g = f h . map f
I finally got around to fixing the name clash bug. It now reports:
g . h = k . g = map
I'd like to see a mix of the two systems. Top level quantifiers
should be optional; they often don't improve readability.
-- Lennart
On Sep 4, 2006, at 04:21 , Janis Voigtlaender wrote:
[EMAIL PROTECTED] wrote:
G'day all.
Quoting Donald Bruce Stewart [EMAIL PROTECTED]:
Get some
