equal
deleted
inserted
replaced
950 nat} and {\tt list}) and ways for introducing new types. The most important |
950 nat} and {\tt list}) and ways for introducing new types. The most important |
951 type construction, the {\tt datatype}, is treated separately in |
951 type construction, the {\tt datatype}, is treated separately in |
952 \S\ref{sec:HOL:datatype}. |
952 \S\ref{sec:HOL:datatype}. |
953 |
953 |
954 \subsection{Product and sum types}\index{*"* type}\index{*"+ type} |
954 \subsection{Product and sum types}\index{*"* type}\index{*"+ type} |
|
955 \label{subsec:prod-sum} |
955 |
956 |
956 \begin{figure}[htbp] |
957 \begin{figure}[htbp] |
957 \begin{constants} |
958 \begin{constants} |
958 \it symbol & \it meta-type & & \it description \\ |
959 \it symbol & \it meta-type & & \it description \\ |
959 \cdx{Pair} & $[\alpha,\beta]\To \alpha\times\beta$ |
960 \cdx{Pair} & $[\alpha,\beta]\To \alpha\times\beta$ |
1574 \mbox{\tt case}~e~\mbox{\tt of} & C_1~x_{11}~\dots~x_{1k_1} & \To & e_1 \\ |
1575 \mbox{\tt case}~e~\mbox{\tt of} & C_1~x_{11}~\dots~x_{1k_1} & \To & e_1 \\ |
1575 \vdots \\ |
1576 \vdots \\ |
1576 \mid & C_m~x_{m1}~\dots~x_{mk_m} & \To & e_m |
1577 \mid & C_m~x_{m1}~\dots~x_{mk_m} & \To & e_m |
1577 \end{array} |
1578 \end{array} |
1578 \] |
1579 \] |
|
1580 where the $x_{ij}$ are either identifiers or nested tuple patterns as in |
|
1581 \S\ref{subsec:prod-sum}. |
1579 \begin{warn} |
1582 \begin{warn} |
1580 In contrast to \ML, {\em all} constructors must be present, their order is |
1583 In contrast to \ML, {\em all} constructors must be present, their order is |
1581 fixed, and nested patterns are not supported. Violating this restriction |
1584 fixed, and nested patterns are not supported (with the exception of tuples). |
1582 results in strange error messages. |
1585 Violating this restriction results in strange error messages. |
1583 \end{warn} |
1586 \end{warn} |
1584 |
1587 |
1585 \underscoreoff |
1588 \underscoreoff |
1586 |
1589 |
1587 \subsection{Defining datatypes} |
1590 \subsection{Defining datatypes} |