doc-src/Ref/defining.tex
changeset 452 395bbf6e55f9
parent 332 01b87a921967
child 711 bb868a30e66f
equal deleted inserted replaced
451:9ebdead316e0 452:395bbf6e55f9
    97 $logic$ &=& $prop$ ~~$|$~~ $fun$ \\\\
    97 $logic$ &=& $prop$ ~~$|$~~ $fun$ \\\\
    98 $aprop$ &=& $id$ ~~$|$~~ $var$
    98 $aprop$ &=& $id$ ~~$|$~~ $var$
    99     ~~$|$~~ $fun^{(\infty)}$ {\tt(} $logic$ {\tt,} \dots {\tt,} $logic$ {\tt)} \\\\
    99     ~~$|$~~ $fun^{(\infty)}$ {\tt(} $logic$ {\tt,} \dots {\tt,} $logic$ {\tt)} \\\\
   100 $fun$ &=& $id$ ~~$|$~~ $var$ ~~$|$~~ {\tt(} $fun$ {\tt)} \\
   100 $fun$ &=& $id$ ~~$|$~~ $var$ ~~$|$~~ {\tt(} $fun$ {\tt)} \\
   101     &$|$& $fun^{(\infty)}$ {\tt(} $logic$ {\tt,} \dots {\tt,} $logic$ {\tt)} \\
   101     &$|$& $fun^{(\infty)}$ {\tt(} $logic$ {\tt,} \dots {\tt,} $logic$ {\tt)} \\
   102     &$|$& $fun^{(\infty)}$ {\tt::} $type$ \\
   102     &$|$& $fun^{(4)}$ {\tt::} $type$ & (4) \\
   103     &$|$& {\tt \%} $idts$ {\tt.} $logic$ & (0) \\\\
   103     &$|$& {\tt \%} $idts$ {\tt.} $logic$ & (0) \\\\
   104 $idts$ &=& $idt$ ~~$|$~~ $idt^{(1)}$ $idts$ \\\\
   104 $idts$ &=& $idt$ ~~$|$~~ $idt^{(1)}$ $idts$ \\\\
   105 $idt$ &=& $id$ ~~$|$~~ {\tt(} $idt$ {\tt)} \\
   105 $idt$ &=& $id$ ~~$|$~~ {\tt(} $idt$ {\tt)} \\
   106     &$|$& $id$ {\tt ::} $type$ & (0) \\\\
   106     &$|$& $id$ {\tt ::} $type$ & (0) \\\\
   107 $type$ &=& $tid$ ~~$|$~~ $tvar$ ~~$|$~~ $tid$ {\tt::} $sort$
   107 $type$ &=& $tid$ ~~$|$~~ $tvar$ ~~$|$~~ $tid$ {\tt::} $sort$
   184 where $c$ is a subclass of \cldx{logic}, several productions are added:
   184 where $c$ is a subclass of \cldx{logic}, several productions are added:
   185 \begin{center}
   185 \begin{center}
   186 \begin{tabular}{rclc}
   186 \begin{tabular}{rclc}
   187 $ty$ &=& $id$ ~~$|$~~ $var$ ~~$|$~~ {\tt(} $ty$ {\tt)} \\
   187 $ty$ &=& $id$ ~~$|$~~ $var$ ~~$|$~~ {\tt(} $ty$ {\tt)} \\
   188   &$|$& $fun^{(\infty)}$ {\tt(} $logic$ {\tt,} \dots {\tt,} $logic$ {\tt)}\\
   188   &$|$& $fun^{(\infty)}$ {\tt(} $logic$ {\tt,} \dots {\tt,} $logic$ {\tt)}\\
   189   &$|$& $ty^{(\infty)}$ {\tt::} $type$\\\\
   189   &$|$& $ty^{(4)}$ {\tt::} $type$ ~~~~~~~ (3) \\\\
   190 $logic$ &=& $ty$
   190 $logic$ &=& $ty$
   191 \end{tabular}
   191 \end{tabular}
   192 \end{center}
   192 \end{center}
   193 
   193 
       
   194 \begin{warn}
       
   195   Type constraints bind very weakly. For example, \verb!x<y::nat! is normally
       
   196   parsed as \verb!(x<y)::nat!, unless \verb$<$ has priority of 4 or less, in
       
   197   which case the string is likely to be ambiguous. The correct form is
       
   198   \verb!x<(y::nat)!.
       
   199 \end{warn}
   194 
   200 
   195 \subsection{Lexical matters}
   201 \subsection{Lexical matters}
   196 The parser does not process input strings directly.  It operates on token
   202 The parser does not process input strings directly.  It operates on token
   197 lists provided by Isabelle's \bfindex{lexer}.  There are two kinds of
   203 lists provided by Isabelle's \bfindex{lexer}.  There are two kinds of
   198 tokens: \bfindex{delimiters} and \bfindex{name tokens}.
   204 tokens: \bfindex{delimiters} and \bfindex{name tokens}.