author lcp Fri, 26 Nov 1993 13:00:35 +0100 changeset 158 c2fcb6c07689 parent 157 8258c26ae084 child 159 3d0324f9417b
Correction to eta-contraction; thanks to Markus W.
--- a/doc-src/Ref/introduction.tex	Fri Nov 26 12:54:58 1993 +0100
+++ b/doc-src/Ref/introduction.tex	Fri Nov 26 13:00:35 1993 +0100
@@ -198,9 +198,10 @@
The {\bf $\eta$-contraction law} asserts $(\lambda x.f(x))\equiv f$,
provided $x$ is not free in ~$f$.  It asserts {\bf extensionality} of
functions: $f\equiv g$ if $f(x)\equiv g(x)$ for all~$x$.  Higher-order
-unification puts terms into a fully $\eta$-expanded form.  For example, if
-$F$ has type $(\tau\To\tau)\To\tau$ then its expanded form is $\lambda -h.F(\lambda x.h(x))$.  By default, the user sees this expanded form.
+unification occasionally puts terms into a fully $\eta$-expanded form.  For
+example, if $F$ has type $(\tau\To\tau)\To\tau$ then its expanded form is
+$\lambda h.F(\lambda x.h(x))$.  By default, the user sees this expanded
+form.

\begin{description}
\item[\ttindexbold{eta_contract} \tt:= true;]