comparison doc/manual.tex @ 1579:e1f4ac9ca34b

Note a parsing restriction in the manual
author Adam Chlipala <adam@chlipala.net>
date Fri, 21 Oct 2011 08:36:10 -0400
parents 7d2aa0ddc531
children 257421857680
comparison
equal deleted inserted replaced
1578:7d2aa0ddc531 1579:e1f4ac9ca34b
424 \\ 424 \\
425 \textrm{Qualified uncapitalized variables} & \hat{x} &::=& x & \textrm{not from a module} \\ 425 \textrm{Qualified uncapitalized variables} & \hat{x} &::=& x & \textrm{not from a module} \\
426 &&& M.x & \textrm{projection from a module} \\ 426 &&& M.x & \textrm{projection from a module} \\
427 \end{array}$$ 427 \end{array}$$
428 428
429 We include both abstraction and application for kind polymorphism, but applications are only inferred internally; they may not be written explicitly in source programs. 429 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).
430 430
431 Modules of the module system are described by \emph{signatures}. 431 Modules of the module system are described by \emph{signatures}.
432 $$\begin{array}{rrcll} 432 $$\begin{array}{rrcll}
433 \textrm{Signatures} & S &::=& \mt{sig} \; s^* \; \mt{end} & \textrm{constant} \\ 433 \textrm{Signatures} & S &::=& \mt{sig} \; s^* \; \mt{end} & \textrm{constant} \\
434 &&& X & \textrm{variable} \\ 434 &&& X & \textrm{variable} \\