# HG changeset patch
# User nipkow
# Date 773601769 -7200
# Node ID 395bbf6e55f96ebaa7fce9d6b1790c8c06a570fe
# Parent  9ebdead316e0f955fc88de7137bbbe342308652f
changed priority of ::

diff -r 9ebdead316e0 -r 395bbf6e55f9 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