summaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
Diffstat (limited to 'doc')
-rw-r--r--doc/manual.tex4
1 files changed, 3 insertions, 1 deletions
diff --git a/doc/manual.tex b/doc/manual.tex
index 2c1cecc2..541dd96b 100644
--- a/doc/manual.tex
+++ b/doc/manual.tex
@@ -380,7 +380,7 @@ $$\begin{array}{rrcll}
&&& \{\kappa\} & \textrm{type-level records} \\
&&& (\kappa\times^+) & \textrm{type-level tuples} \\
&&& X & \textrm{variable} \\
- &&& X \longrightarrow k & \textrm{kind-polymorphic type-level function} \\
+ &&& X \longrightarrow \kappa & \textrm{kind-polymorphic type-level function} \\
&&& \_\_ & \textrm{wildcard} \\
&&& (\kappa) & \textrm{explicit precedence} \\
\end{array}$$
@@ -549,6 +549,8 @@ A tuple type $\tau_1 \times \ldots \times \tau_n$ expands to a record type $\{1
In general, several adjacent $\lambda$ forms may be combined into one, and kind and type annotations may be omitted, in which case they are implicitly included as wildcards. More formally, for constructor-level abstractions, we can define a new non-terminal $b ::= x \mid (x :: \kappa) \mid X$ and allow composite abstractions of the form $\lambda b^+ \Rightarrow c$, elaborating into the obvious sequence of one core $\lambda$ per element of $b^+$.
+Further, the signature item or declaration syntax $\mt{con} \; x \; b^+ = c$ is shorthand for wrapping of the appropriate $\lambda$s around the righthand side $c$. The $b$ elements may not include $X$, and there may also be an optional $:: \kappa$ before the $=$.
+
In some contexts, the parser isn't happy with token sequences like $x :: \_$, to indicate a constructor variable of wildcard kind. In such cases, write the second two tokens as $::\hspace{-.05in}\_$, with no intervening spaces. Analogous syntax $:::\hspace{-.05in}\_$ is available for implicit constructor arguments.
For any signature item or declaration that defines some entity to be equal to $A$ with classification annotation $B$ (e.g., $\mt{val} \; x : B = A$), $B$ and the preceding colon (or similar punctuation) may be omitted, in which case it is filled in as a wildcard.