|
8745
|
1 |
(*<*)
|
|
|
2 |
theory fakenat = Main:;
|
|
|
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 |
(*>*)
|