equal
deleted
inserted
replaced
91 |
91 |
92 fun mull :: "nat \<Rightarrow> nat \<Rightarrow> nat" where |
92 fun mull :: "nat \<Rightarrow> nat \<Rightarrow> nat" where |
93 "mull 0 0 = 0" | |
93 "mull 0 0 = 0" | |
94 "mull m 0 = 0" | |
94 "mull m 0 = 0" | |
95 (**"mull m 1 = m" | **) |
95 (**"mull m 1 = m" | **) |
96 "mull m n = m*n" |
96 (**"mull m (1::nat) = m" | **) |
|
97 (**"mull m (suc(0)) = m" | **) |
|
98 "mull m n = mull m (n-(1::nat))" |
97 |
99 |
|
100 (**Define a function that counts the |
|
101 number of occurrences of an element in a list **) |
98 (** |
102 (** |
99 fun count :: "'a\<Rightarrow>'a list\<Rightarrow>nat" where |
103 fun count :: "'a\<Rightarrow>'a list\<Rightarrow>nat" where |
100 "count " |
104 "count " |
101 **) |
105 **) |
102 |
106 |