From 30f4db7bbc1b9ccfd92c2b516ffcd638bc5ae5f9 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 10 Oct 2010 20:33:10 -0400 Subject: :::_ notation; switch to TooDeep error message --- doc/manual.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc') diff --git a/doc/manual.tex b/doc/manual.tex index 9dbdb505..ebeb2d55 100644 --- a/doc/manual.tex +++ b/doc/manual.tex @@ -495,7 +495,7 @@ 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. +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. -- cgit v1.2.3