changeset 8929 | 4829556a56f8 |
parent 5183 | 89f162de39cf |
child 8939 | 23f85299689f |
8928:1d3bf47a4ecc | 8929:4829556a56f8 |
---|---|
24 |
24 |
25 primrec |
25 primrec |
26 mult_0 "0 * n = 0" |
26 mult_0 "0 * n = 0" |
27 mult_Suc "Suc m * n = n + (m * n)" |
27 mult_Suc "Suc m * n = n + (m * n)" |
28 |
28 |
29 (*We overload the constant for all + types, but unfortunately there's no |
|
30 overloaded 0...*) |
|
31 consts sum_below :: [nat=>'a, nat] => ('a::plus) |
|
32 primrec |
|
33 sum_below_0 "sum_below f 0 = 0" |
|
34 sum_below_Suc "sum_below f (Suc n) = f(n) + sum_below f n" |
|
35 |
|
29 end |
36 end |