summaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2011-10-21 08:36:10 -0400
committerGravatar Adam Chlipala <adam@chlipala.net>2011-10-21 08:36:10 -0400
commitb24fbf5d255d3e32338cb43f447a8369deef4b0b (patch)
treee501d1b0c252da0c6c0d94cdbb8b7a6af6f16243 /doc
parente60654674f6c4acd3edb8fe7e6df5139a6d43d21 (diff)
Note a parsing restriction in the manual
Diffstat (limited to 'doc')
-rw-r--r--doc/manual.tex2
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/manual.tex b/doc/manual.tex
index 872dca93..71df6ccc 100644
--- a/doc/manual.tex
+++ b/doc/manual.tex
@@ -426,7 +426,7 @@ $$\begin{array}{rrcll}
&&& M.x & \textrm{projection from a module} \\
\end{array}$$
-We include both abstraction and application for kind polymorphism, but applications are only inferred internally; they may not be written explicitly in source programs.
+We include both abstraction and application for kind polymorphism, but applications are only inferred internally; they may not be written explicitly in source programs. Also, in the ``known-length type-level record'' form, in $c_1 = c_2$ terms, the parser currently only allows $c_1$ to be of the forms $X$ (as a shorthand for $\#X$) or $x$, or a natural number to stand for the corresponding field name (e.g., for tuples).
Modules of the module system are described by \emph{signatures}.
$$\begin{array}{rrcll}