| author | wenzelm |
| Tue, 17 Sep 2024 18:49:46 +0200 | |
| changeset 80898 | 71756d95b7df |
| parent 67406 | 23307fd33906 |
| child 80914 | d97fdabd9e2b |
| permissions | -rw-r--r-- |
| 8745 | 1 |
(*<*) |
| 58860 | 2 |
theory fakenat imports Main begin |
| 8745 | 3 |
(*>*) |
4 |
||
| 67406 | 5 |
text\<open>\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: |
| 67406 | 9 |
\<close> |
| 8745 | 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 |
(*>*) |