equal
deleted
inserted
replaced
15 Thanks to Sloane's On-Line Encyclopedia of Integer Sequences, |
15 Thanks to Sloane's On-Line Encyclopedia of Integer Sequences, |
16 http://www.research.att.com/~njas/sequences/ |
16 http://www.research.att.com/~njas/sequences/ |
17 *) |
17 *) |
18 |
18 |
19 |
19 |
20 theory NatSum = Main: |
20 theory NatSum imports Main begin |
21 |
21 |
22 consts sum :: "[i=>i, i] => i" |
22 consts sum :: "[i=>i, i] => i" |
23 primrec |
23 primrec |
24 "sum (f,0) = #0" |
24 "sum (f,0) = #0" |
25 "sum (f, succ(n)) = f($#n) $+ sum(f,n)" |
25 "sum (f, succ(n)) = f($#n) $+ sum(f,n)" |