aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMatej Kosik2015-10-29 17:34:05 +0100
committerHugo Herbelin2015-12-10 09:35:10 +0100
commita388e5401c2f83f4068314087e67d751acb59d17 (patch)
treec727bf53fc356f021dfcbebeff7826c6207aab5e
parentc56035c2850fe09fc5ef6389e58de28109ad5a93 (diff)
GRAMMAR
-rw-r--r--doc/refman/RefMan-cic.tex2
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$.