equal
deleted
inserted
replaced
196 eta_contract: bool ref \hfill{\bf initially false} |
196 eta_contract: bool ref \hfill{\bf initially false} |
197 \end{ttbox} |
197 \end{ttbox} |
198 The {\bf $\eta$-contraction law} asserts $(\lambda x.f(x))\equiv f$, |
198 The {\bf $\eta$-contraction law} asserts $(\lambda x.f(x))\equiv f$, |
199 provided $x$ is not free in ~$f$. It asserts {\bf extensionality} of |
199 provided $x$ is not free in ~$f$. It asserts {\bf extensionality} of |
200 functions: $f\equiv g$ if $f(x)\equiv g(x)$ for all~$x$. Higher-order |
200 functions: $f\equiv g$ if $f(x)\equiv g(x)$ for all~$x$. Higher-order |
201 unification puts terms into a fully $\eta$-expanded form. For example, if |
201 unification occasionally puts terms into a fully $\eta$-expanded form. For |
202 $F$ has type $(\tau\To\tau)\To\tau$ then its expanded form is $\lambda |
202 example, if $F$ has type $(\tau\To\tau)\To\tau$ then its expanded form is |
203 h.F(\lambda x.h(x))$. By default, the user sees this expanded form. |
203 $\lambda h.F(\lambda x.h(x))$. By default, the user sees this expanded |
|
204 form. |
204 |
205 |
205 \begin{description} |
206 \begin{description} |
206 \item[\ttindexbold{eta_contract} \tt:= true;] |
207 \item[\ttindexbold{eta_contract} \tt:= true;] |
207 makes Isabelle perform $\eta$-contractions before printing, so that |
208 makes Isabelle perform $\eta$-contractions before printing, so that |
208 $\lambda h.F(\lambda x.h(x))$ appears simply as~$F$. The |
209 $\lambda h.F(\lambda x.h(x))$ appears simply as~$F$. The |