diff options
| author | Matej Kosik | 2015-10-29 17:34:05 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-12-10 09:35:10 +0100 |
| commit | a388e5401c2f83f4068314087e67d751acb59d17 (patch) | |
| tree | c727bf53fc356f021dfcbebeff7826c6207aab5e | |
| parent | c56035c2850fe09fc5ef6389e58de28109ad5a93 (diff) | |
GRAMMAR
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index a008bd19a5..b7bbf7125f 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -416,7 +416,7 @@ $$\WTEGRED{\kw{let}~x:=u~\kw{in}~t}{\triangleright_{\zeta}}{\subst{t}{x}{u}}$$ \index{eta-conversion@$\eta$-conversion} %\index{eta-reduction@$\eta$-reduction} } -An other important concept is $\eta$-conversion. It is to identify any +Another important concept is $\eta$-conversion. It is to identify any term $t$ of functional type $\forall x:T, U$ with its so-called $\eta$-expansion $\lb x:T\mto (t\ x)$ for $x$ an arbitrary variable name fresh in $t$. |
