WhoCites Definitions mb list 2 Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Who Cites double sum?
double_sumDef sum(f(x;y) | x < ny < m) == sum(sum(f(x;y) | y < m) | x < n)
Thm* n,m:f:(nm). sum(f(x,y) | x < ny < m 
sumDef sum(f(x) | x < k) == primrec(k;0;x,nn+f(x))
Thm* n:f:(n). sum(f(x) | x < n 
primrecDef primrec(n;b;c) == if n=0 b else c(n-1,primrec(n-1;b;c)) fi  (recursive)
Thm* T:Type, n:b:Tc:(nTT). primrec(n;b;c T
eq_intDef i=j == if i=j true ; false fi
Thm* i,j:. (i=j 

Syntax:sum(f(x;y) | x < ny < m) has structure: double_sum(nmx,y.f(x;y))

About:
boolbfalsebtrueifthenelseintnatural_numberaddsubtractint_eq
lambdaapplyfunctionrecursive_def_noticeuniversememberall!abstraction
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

WhoCites Definitions mb list 2 Sections MarkB generic Doc