diff options
| author | herbelin | 2001-04-10 03:09:58 +0000 |
|---|---|---|
| committer | herbelin | 2001-04-10 03:09:58 +0000 |
| commit | 1bf6166b5e4247e18602ac2967a919fbc02403b4 (patch) | |
| tree | a1c0e2903d18a8880d56be36a9555ffcb7744810 | |
| parent | 377ed722c489f927b9d68503c07f2c66631217f3 (diff) | |
typo
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8184 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | doc/RefMan-gal.tex | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/doc/RefMan-gal.tex b/doc/RefMan-gal.tex index b38a589d02..9a1da4bd38 100644 --- a/doc/RefMan-gal.tex +++ b/doc/RefMan-gal.tex @@ -380,6 +380,7 @@ abstraction when they can be synthetized by the system. assumptions. Obviously, this is expanded into unary abstractions separated by let-in's. + \subsection{Products} \index{products} @@ -416,7 +417,14 @@ associativity is to the left. binding of \term$_1$ to the variable $\ident$ in \term$_2$. \medskip -Rem The expression {\tt [}{\ident}{\tt :=}{\term$_1$}{\tt :}{\type}{\tt ]}{\term$_2$} is equivalent to {\tt [}{\ident}{\tt :=(}{\term$_1$}{\tt ::}{\type}{\tt )]}{\term$_2$}. +\Rem The expression {\tt [}{\ident}{\tt :=}{\term$_1$}{\tt +:}{\type}{\tt ]}{\term$_2$} is equivalent to {\tt [}{\ident}{\tt +:=(}{\term$_1$}{\tt ::}{\type}{\tt )]}{\term$_2$}. + +\Rem An alternative equivalent syntax for let-in is {\tt let} {\ident} +{\tt =} {\term} {\tt in} {\term}. For historical reasons, the syntax +{\tt [} {\ident} {\tt =} {\term} {\tt ]} {\term} is also available but +is not recommended. \subsection{Definition by case analysis} \index{Cases@{\tt Cases\ldots of\ldots end}} |