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 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 /sfa/Nuprl/Shared/Xindentation_hack_doc.html

WhoCites Definitions mb list 2 Sections MarkB generic Doc