WhoCites Definitions mb nat Sections MarkB generic Search Doc
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
Who Cites primrec?
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:primrec(n;b;c) has structure: primrec(nbc)

About:
boolbfalsebtrueifthenelseintnatural_numbersubtractint_eq
applyfunctionrecursive_def_noticeuniversememberall!abstraction
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

WhoCites Definitions mb nat Sections MarkB generic Search Doc