diff options
author | Adam Chlipala <adam@chlipala.net> | 2010-10-10 13:07:38 -0400 |
---|---|---|
committer | Adam Chlipala <adam@chlipala.net> | 2010-10-10 13:07:38 -0400 |
commit | d8bc26c9647d2b45009f6538bc2a69508c983449 (patch) | |
tree | 1d0f355dec824a81d80e9e838e0cae8845f8e179 /doc/manual.tex | |
parent | 975b1f43784dfc1769ec93dd5dd408434791464e (diff) |
Flex kinds for type-level tuples; ::_ notation
Diffstat (limited to 'doc/manual.tex')
-rw-r--r-- | doc/manual.tex | 2 |
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. |