equal
deleted
inserted
replaced
2 theory Option2 = Main: |
2 theory Option2 = Main: |
3 hide const None Some |
3 hide const None Some |
4 hide type option |
4 hide type option |
5 (*>*) |
5 (*>*) |
6 |
6 |
7 text{*\indexbold{*option}\indexbold{*None}\indexbold{*Some} |
7 text{*\indexbold{*option (type)}\indexbold{*None (constant)}% |
|
8 \indexbold{*Some (constant)} |
8 Our final datatype is very simple but still eminently useful: |
9 Our final datatype is very simple but still eminently useful: |
9 *} |
10 *} |
10 |
11 |
11 datatype 'a option = None | Some 'a; |
12 datatype 'a option = None | Some 'a; |
12 |
13 |