x,n. n+f(x))
n:
, f:(n
). sum(f(x) | x < n) 
0
b else c(n-1,primrec(n-1;b;c)) fi (recursive)T:Type, n:, b:T, c:(nTT). primrec(n;b;c) Tj == if i=j true ; false fii,j:. (i=j) 
| Who Cites sum? | |
| sum | Def sum(f(x) | x < k) == primrec(k;0;x,n. n+f(x)) |
| Thm* n:, f:(n). sum(f(x) | x < n) | |
| primrec | Def primrec(n;b;c) == if n=0 b else c(n-1,primrec(n-1;b;c)) fi (recursive) |
| Thm* T:Type, n:, b:T, c:(nTT). primrec(n;b;c) T | |
| eq_int | Def i=j == if i=j true ; false fi |
| Thm* i,j:. (i=j) |
| Syntax: | sum(f(x) | x < k) | has structure: | sum(k; x.f(x)) |
About:
 |  |  |  |  |  |  |  |  |
 |  |  |  |  |  |  |  |