equal
deleted
inserted
replaced
33 There is also the type \tydx{unit}, which contains exactly one |
33 There is also the type \tydx{unit}, which contains exactly one |
34 element denoted by~\cdx{()}. This type can be viewed |
34 element denoted by~\cdx{()}. This type can be viewed |
35 as a degenerate product with 0 components. |
35 as a degenerate product with 0 components. |
36 \item |
36 \item |
37 Products, like type \isa{nat}, are datatypes, which means |
37 Products, like type \isa{nat}, are datatypes, which means |
38 in particular that \isa{induct{\isacharunderscore}tac} and \isa{case{\isacharunderscore}tac} are applicable to |
38 in particular that \isa{induct{\isaliteral{5F}{\isacharunderscore}}tac} and \isa{case{\isaliteral{5F}{\isacharunderscore}}tac} are applicable to |
39 terms of product type. |
39 terms of product type. |
40 Both split the term into a number of variables corresponding to the tuple structure |
40 Both split the term into a number of variables corresponding to the tuple structure |
41 (up to 7 components). |
41 (up to 7 components). |
42 \item |
42 \item |
43 Tuples with more than two or three components become unwieldy; |
43 Tuples with more than two or three components become unwieldy; |