| author | huffman |
| Tue, 24 Feb 2009 08:20:14 -0800 | |
| changeset 30080 | 4cf42465b3da |
| parent 16417 | 9bc16273c2d4 |
| permissions | -rw-r--r-- |
| 8745 | 1 |
(*<*) |
| 16417 | 2 |
theory fakenat imports Main begin; |
| 8745 | 3 |
(*>*) |
4 |
||
5 |
text{*\noindent
|
|
| 11418 | 6 |
The type \tydx{nat} of natural
|
7 |
numbers is predefined to have the constructors \cdx{0} and~\cdx{Suc}. It behaves as if it were declared like this:
|
|
| 8745 | 8 |
*} |
9 |
||
| 9541 | 10 |
datatype nat = 0 | Suc nat |
| 8745 | 11 |
(*<*) |
12 |
end |
|
13 |
(*>*) |