equal
deleted
inserted
replaced
22 but it is often simpler to use @{text option}. For an application see |
22 but it is often simpler to use @{text option}. For an application see |
23 \S\ref{sec:Trie}. |
23 \S\ref{sec:Trie}. |
24 *} |
24 *} |
25 (*<*) |
25 (*<*) |
26 (* |
26 (* |
27 constdefs |
27 definition infplus :: "nat option \<Rightarrow> nat option \<Rightarrow> nat option" where |
28 infplus :: "nat option \<Rightarrow> nat option \<Rightarrow> nat option" |
|
29 "infplus x y \<equiv> case x of None \<Rightarrow> None |
28 "infplus x y \<equiv> case x of None \<Rightarrow> None |
30 | Some m \<Rightarrow> (case y of None \<Rightarrow> None | Some n \<Rightarrow> Some(m+n))" |
29 | Some m \<Rightarrow> (case y of None \<Rightarrow> None | Some n \<Rightarrow> Some(m+n))" |
31 |
30 |
32 *) |
31 *) |
33 end |
32 end |