equal
deleted
inserted
replaced
292 qualified internal form. |
292 qualified internal form. |
293 |
293 |
294 \end{ttdescription} |
294 \end{ttdescription} |
295 |
295 |
296 |
296 |
297 \subsection{$\eta$-contraction before printing} |
297 \subsection{Eta-contraction before printing} |
298 \begin{ttbox} |
298 \begin{ttbox} |
299 eta_contract: bool ref \hfill{\bf initially false} |
299 eta_contract: bool ref \hfill{\bf initially false} |
300 \end{ttbox} |
300 \end{ttbox} |
301 The {\bf $\eta$-contraction law} asserts $(\lambda x.f(x))\equiv f$, |
301 The {\bf $\eta$-contraction law} asserts $(\lambda x.f(x))\equiv f$, |
302 provided $x$ is not free in ~$f$. It asserts {\bf extensionality} of |
302 provided $x$ is not free in ~$f$. It asserts {\bf extensionality} of |