equal
deleted
inserted
replaced
20 as a degenerate product with 0 components. |
20 as a degenerate product with 0 components. |
21 \item |
21 \item |
22 Products, like type @{typ nat}, are datatypes, which means |
22 Products, like type @{typ nat}, are datatypes, which means |
23 in particular that @{text induct_tac} and @{text case_tac} are applicable to |
23 in particular that @{text induct_tac} and @{text case_tac} are applicable to |
24 terms of product type. |
24 terms of product type. |
|
25 Both replace the term by tuple of variables. |
25 \item |
26 \item |
26 Instead of tuples with many components (where ``many'' is not much above 2), |
27 Tuples with more than two or three components become unwieldy; |
27 it is preferable to use records. |
28 records are preferable. |
28 \end{itemize} |
29 \end{itemize} |
29 For more information on pairs and records see Chapter~\ref{ch:more-types}. |
30 For more information on pairs and records see Chapter~\ref{ch:more-types}. |
30 *} |
31 *} |
31 (*<*) |
32 (*<*) |
32 end |
33 end |