equal
deleted
inserted
replaced
20 The type \tydx{nat} of natural |
20 The type \tydx{nat} of natural |
21 numbers is predefined to have the constructors \cdx{0} and~\cdx{Suc}. It behaves as if it were declared like this:% |
21 numbers is predefined to have the constructors \cdx{0} and~\cdx{Suc}. It behaves as if it were declared like this:% |
22 \end{isamarkuptext}% |
22 \end{isamarkuptext}% |
23 \isamarkuptrue% |
23 \isamarkuptrue% |
24 \isacommand{datatype}\isamarkupfalse% |
24 \isacommand{datatype}\isamarkupfalse% |
25 \ nat\ {\isacharequal}\ {\isadigit{0}}\ {\isacharbar}\ Suc\ nat% |
25 \ nat\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}\ {\isaliteral{7C}{\isacharbar}}\ Suc\ nat% |
26 \isadelimtheory |
26 \isadelimtheory |
27 % |
27 % |
28 \endisadelimtheory |
28 \endisadelimtheory |
29 % |
29 % |
30 \isatagtheory |
30 \isatagtheory |