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 mklist?
mklistDef mklist(n;f) == primrec(n;nil;i,ll @ [(f(i))])
Thm* T:Type, n:f:(nT). mklist(n;f T List
appendDef as @ bs == Case of as; nil  bs ; a.as'  [a / (as' @ bs)]  (recursive)
Thm* T:Type, as,bs:T List. (as @ bs T List
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:mklist(n;f) has structure: mklist(nf)

About:
listconsconsnillist_indbool
bfalsebtrueifthenelseintnatural_numbersubtractint_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