"This term is not in normal form" ; so what ?
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!