equal
deleted
inserted
replaced
12 fun null (A_:'a null) = #null A_; |
12 fun null (A_:'a null) = #null A_; |
13 |
13 |
14 fun head B_ (x :: xs) = x |
14 fun head B_ (x :: xs) = x |
15 | head B_ [] = null B_; |
15 | head B_ [] = null B_; |
16 |
16 |
17 fun null_option () = {null = NONE} : ('a option) null; |
17 val null_option : 'a option = NONE; |
|
18 |
|
19 fun null_optiona () = {null = null_option} : ('a option) null; |
18 |
20 |
19 val dummy : Nat.nat option = |
21 val dummy : Nat.nat option = |
20 head (null_option ()) [SOME (Nat.Suc Nat.Zero_nat), NONE]; |
22 head (null_optiona ()) [SOME (Nat.Suc Nat.Zero_nat), NONE]; |
21 |
23 |
22 end; (*struct Codegen*) |
24 end; (*struct Codegen*) |