equal
deleted
inserted
replaced
1 structure Nat = |
|
2 struct |
|
3 |
|
4 datatype nat = Suc of nat | Zero_nat; |
|
5 |
|
6 end; (*struct Nat*) |
|
7 |
|
8 structure Codegen = |
|
9 struct |
|
10 |
|
11 type 'a null = {null : 'a}; |
|
12 fun null (A_:'a null) = #null A_; |
|
13 |
|
14 fun head A_ (x :: xs) = x |
|
15 | head A_ [] = null A_; |
|
16 |
|
17 val null_option : 'a option = NONE; |
|
18 |
|
19 fun null_optiona () = {null = null_option} : ('a option) null; |
|
20 |
|
21 val dummy : Nat.nat option = |
|
22 head (null_optiona ()) [SOME (Nat.Suc Nat.Zero_nat), NONE]; |
|
23 |
|
24 end; (*struct Codegen*) |
|