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 sum?
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) | x < k) has structure: sum(kx.f(x))

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