"This term is not in normal form" ; so what ?
Hi,
I don't understand why the following refuse to compile.
signature TMP =
a : type ;
M, N : a ;
t = (Lambda x. M) N : a ;
end
I sure understand the error message "This term is not in normal form". But then why the following compiles?
signature TMP =
a : type ;
M, N : a ;
u = (Lambda x. M) : a => a ;
t = u N : a ;
end
Besides, assume N is not a value yet and will only become so through epsilon-reductions. ACGtk doesn't account for such reductions — which may be for the best. Then the first t
is in normal form w.r.t. beta-eta-reductions. This hypothetical case is how I stumble on that issue.
Please free us from that normative straightjacket!