equal
deleted
inserted
replaced
21 abbreviation |
21 abbreviation |
22 empty :: "'a ~=> 'b" where |
22 empty :: "'a ~=> 'b" where |
23 "empty == %x. None" |
23 "empty == %x. None" |
24 |
24 |
25 definition |
25 definition |
26 map_comp :: "('b ~=> 'c) => ('a ~=> 'b) => ('a ~=> 'c)" (infixl "o'_m" 55) where |
26 map_comp :: "('b ~=> 'c) => ('a ~=> 'b) => ('a ~=> 'c)" (infixl "o'_m" 55) where |
27 "f o_m g = (\<lambda>k. case g k of None \<Rightarrow> None | Some v \<Rightarrow> f v)" |
27 "f o_m g = (\<lambda>k. case g k of None \<Rightarrow> None | Some v \<Rightarrow> f v)" |
28 |
28 |
29 notation (xsymbols) |
29 notation (xsymbols) |
30 map_comp (infixl "\<circ>\<^sub>m" 55) |
30 map_comp (infixl "\<circ>\<^sub>m" 55) |
31 |
31 |