| author | wenzelm |
| Thu, 29 Jun 2017 21:43:55 +0200 | |
| changeset 66223 | a6fdb22b0ce2 |
| 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 |
(*>*) |