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} : ('b option) null; |
17 fun null_option () = {null = NONE} : ('a option) null; |
18 |
18 |
19 val dummy : Nat.nat option = |
19 val dummy : Nat.nat option = |
20 head (null_option ()) [SOME (Nat.Suc Nat.Zero_nat), NONE]; |
20 head (null_option ()) [SOME (Nat.Suc Nat.Zero_nat), NONE]; |
21 |
21 |
22 end; (*struct Codegen*) |
22 end; (*struct Codegen*) |