summaryrefslogtreecommitdiff
path: root/doc/manual.tex
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2010-10-10 13:07:38 -0400
committerGravatar Adam Chlipala <adam@chlipala.net>2010-10-10 13:07:38 -0400
commitd8bc26c9647d2b45009f6538bc2a69508c983449 (patch)
tree1d0f355dec824a81d80e9e838e0cae8845f8e179 /doc/manual.tex
parent975b1f43784dfc1769ec93dd5dd408434791464e (diff)
Flex kinds for type-level tuples; ::_ notation
Diffstat (limited to 'doc/manual.tex')
-rw-r--r--doc/manual.tex2
1 files changed, 2 insertions, 0 deletions
diff --git a/doc/manual.tex b/doc/manual.tex
index 98b3b63c..9dbdb505 100644
--- a/doc/manual.tex
+++ b/doc/manual.tex
@@ -495,6 +495,8 @@ A tuple type $(\tau_1, \ldots, \tau_n)$ expands to a record type $\{1 = \tau_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^+$.
+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.
+
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.
A signature item or declaration $\mt{type} \; x$ or $\mt{type} \; x = \tau$ is elaborated into $\mt{con} \; x :: \mt{Type}$ or $\mt{con} \; x :: \mt{Type} = \tau$, respectively.