summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

doc-src/Ref/introduction.tex

changeset 158 | c2fcb6c07689 |

parent 149 | caa7a52ff46f |

child 159 | 3d0324f9417b |

--- 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;]