diff options
| author | Maxime Dénès | 2016-06-27 12:32:03 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-06-27 12:32:03 +0200 |
| commit | c1caa158add73e6e6028ade81a0cb4540a845d18 (patch) | |
| tree | e6cd36fc03ae7a79d9b65f08b0295bedc485f855 /doc | |
| parent | a553126c9e0984f38b1a15f2db60458813a177c9 (diff) | |
| parent | c6d9d4fb142ef42634be25b60c0995b541e86629 (diff) | |
Merge branch 'funpattern' into trunk. Was PR#142: Binder syntax.
Diffstat (limited to 'doc')
| -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 fcccd9cb4b..99eee44e03 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 |