changeset 19 | 66c9c06c0f0e |
parent 17 | a5427713eef4 |
child 20 | c11651bbebf5 |
18:8c9349065477 | 19:66c9c06c0f0e |
---|---|
102 (** |
102 (** |
103 fun count :: "'a\<Rightarrow>'a list\<Rightarrow>nat" where |
103 fun count :: "'a\<Rightarrow>'a list\<Rightarrow>nat" where |
104 "count " |
104 "count " |
105 **) |
105 **) |
106 |
106 |
107 fun sum :: "nat \<Rightarrow> nat" where |
|
108 "sum n = 0 + \<dots> + n" |
|
109 (* prove n = n * (n + 1) div 2 *) |
|
107 |
110 |
108 |
111 |
109 |
112 |
110 |
113 |
111 |
114 |
112 |
115 |
113 |
116 |
114 |
117 |
115 |
118 |
119 |
|
120 |