equal
deleted
inserted
replaced
299 \end{ttdescription} |
299 \end{ttdescription} |
300 |
300 |
301 |
301 |
302 \subsection{Eta-contraction before printing} |
302 \subsection{Eta-contraction before printing} |
303 \begin{ttbox} |
303 \begin{ttbox} |
304 eta_contract: bool ref \hfill{\bf initially false} |
304 eta_contract: bool ref |
305 \end{ttbox} |
305 \end{ttbox} |
306 The {\bf $\eta$-contraction law} asserts $(\lambda x.f(x))\equiv f$, |
306 The {\bf $\eta$-contraction law} asserts $(\lambda x.f(x))\equiv f$, |
307 provided $x$ is not free in ~$f$. It asserts {\bf extensionality} of |
307 provided $x$ is not free in ~$f$. It asserts {\bf extensionality} of |
308 functions: $f\equiv g$ if $f(x)\equiv g(x)$ for all~$x$. Higher-order |
308 functions: $f\equiv g$ if $f(x)\equiv g(x)$ for all~$x$. Higher-order |
309 unification frequently puts terms into a fully $\eta$-expanded form. For |
309 unification frequently puts terms into a fully $\eta$-expanded form. For |