author | wenzelm |
Mon, 21 Aug 2017 17:15:26 +0200 | |
changeset 66475 | d8e0fd64216f |
parent 58860 | fee7cfa69c50 |
child 67406 | 23307fd33906 |
permissions | -rw-r--r-- |
8745 | 1 |
(*<*) |
58860 | 2 |
theory fakenat imports Main begin |
8745 | 3 |
(*>*) |
4 |
||
5 |
text{*\noindent |
|
11418 | 6 |
The type \tydx{nat} of natural |
56260
3d79c132e657
modernized approximation, avoiding bad name binding;
wenzelm
parents:
48985
diff
changeset
|
7 |
numbers is predefined to have the constructors \cdx{0} and~\cdx{Suc}. |
3d79c132e657
modernized approximation, avoiding bad name binding;
wenzelm
parents:
48985
diff
changeset
|
8 |
It behaves approximately as if it were declared like this: |
8745 | 9 |
*} |
10 |
||
56260
3d79c132e657
modernized approximation, avoiding bad name binding;
wenzelm
parents:
48985
diff
changeset
|
11 |
datatype nat = zero ("0") | Suc nat |
8745 | 12 |
(*<*) |
13 |
end |
|
14 |
(*>*) |