diff options
Diffstat (limited to 'doc/refman/RefMan-gal.tex')
| -rw-r--r-- | doc/refman/RefMan-gal.tex | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex index fcccd9cb4..99eee44e0 100644 --- a/doc/refman/RefMan-gal.tex +++ b/doc/refman/RefMan-gal.tex @@ -273,6 +273,7 @@ called \CIC). The formal presentation of {\CIC} is given in Chapter {\binder} & ::= & {\name} & (\ref{Binders}) \\ & $|$ & {\tt (} \nelist{\name}{} {\tt :} {\term} {\tt )} &\\ & $|$ & {\tt (} {\name} {\typecstr} {\tt :=} {\term} {\tt )} &\\ + & $|$ & {\tt '} {\pattern} &\\ & & &\\ {\name} & ::= & {\ident} &\\ & $|$ & {\tt \_} &\\ @@ -410,7 +411,8 @@ bound variable cannot be synthesized by the system, it can be specified with the notation {\tt (}\,{\ident}\,{\tt :}\,{\type}\,{\tt )}. There is also a notation for a sequence of binding variables sharing the same type: {\tt (}\,{\ident$_1$}\ldots{\ident$_n$}\,{\tt -:}\,{\type}\,{\tt )}. +:}\,{\type}\,{\tt )}. A binder can also be any pattern prefixed by a quote, +e.g. {\tt '(x,y)}. Some constructions allow the binding of a variable to value. This is called a ``let-binder''. The entry {\binder} of the grammar accepts |