changed priority of ::
authornipkow
Thu, 07 Jul 1994 19:22:49 +0200
changeset 452 395bbf6e55f9
parent 451 9ebdead316e0
child 453 d4e82b3a06c9
changed priority of ::
doc-src/Ref/defining.tex
--- a/doc-src/Ref/defining.tex	Wed Jul 06 14:39:32 1994 +0200
+++ b/doc-src/Ref/defining.tex	Thu Jul 07 19:22:49 1994 +0200
@@ -99,7 +99,7 @@
     ~~$|$~~ $fun^{(\infty)}$ {\tt(} $logic$ {\tt,} \dots {\tt,} $logic$ {\tt)} \\\\
 $fun$ &=& $id$ ~~$|$~~ $var$ ~~$|$~~ {\tt(} $fun$ {\tt)} \\
     &$|$& $fun^{(\infty)}$ {\tt(} $logic$ {\tt,} \dots {\tt,} $logic$ {\tt)} \\
-    &$|$& $fun^{(\infty)}$ {\tt::} $type$ \\
+    &$|$& $fun^{(4)}$ {\tt::} $type$ & (4) \\
     &$|$& {\tt \%} $idts$ {\tt.} $logic$ & (0) \\\\
 $idts$ &=& $idt$ ~~$|$~~ $idt^{(1)}$ $idts$ \\\\
 $idt$ &=& $id$ ~~$|$~~ {\tt(} $idt$ {\tt)} \\
@@ -186,11 +186,17 @@
 \begin{tabular}{rclc}
 $ty$ &=& $id$ ~~$|$~~ $var$ ~~$|$~~ {\tt(} $ty$ {\tt)} \\
   &$|$& $fun^{(\infty)}$ {\tt(} $logic$ {\tt,} \dots {\tt,} $logic$ {\tt)}\\
-  &$|$& $ty^{(\infty)}$ {\tt::} $type$\\\\
+  &$|$& $ty^{(4)}$ {\tt::} $type$ ~~~~~~~ (3) \\\\
 $logic$ &=& $ty$
 \end{tabular}
 \end{center}
 
+\begin{warn}
+  Type constraints bind very weakly. For example, \verb!x<y::nat! is normally
+  parsed as \verb!(x<y)::nat!, unless \verb$<$ has priority of 4 or less, in
+  which case the string is likely to be ambiguous. The correct form is
+  \verb!x<(y::nat)!.
+\end{warn}
 
 \subsection{Lexical matters}
 The parser does not process input strings directly.  It operates on token