equal
deleted
inserted
replaced
40 sum_map |
40 sum_map |
41 where |
41 where |
42 "sum_map f1 f2 (Inl a) = Inl (f1 a)" |
42 "sum_map f1 f2 (Inl a) = Inl (f1 a)" |
43 | "sum_map f1 f2 (Inr a) = Inr (f2 a)" |
43 | "sum_map f1 f2 (Inr a) = Inr (f2 a)" |
44 |
44 |
45 |
|
46 |
|
47 |
|
48 |
|
49 fun |
45 fun |
50 noption_map::"('a \<Rightarrow> 'b) \<Rightarrow> ('a noption) \<Rightarrow> ('b noption)" |
46 noption_map::"('a \<Rightarrow> 'b) \<Rightarrow> ('a noption) \<Rightarrow> ('b noption)" |
51 where |
47 where |
52 "noption_map f (nSome x) = nSome (f x)" |
48 "noption_map f (nSome x) = nSome (f x)" |
53 | "noption_map f nNone = nNone" |
49 | "noption_map f nNone = nNone" |