WhoCites Definitions MarkB generic Sections NuprlLIB Doc

Who Cites mklist?
mklistDef mklist(n;f) == primrec(n;nil;i,l. l @ [(f(i))])
Thm* T:Type, n:, f:(nT). mklist(n;f) T List
append Def as @ bs == Case of as; nil bs ; a.as' [a / (as' @ bs)] (recursive)
Thm* T:Type, as,bs:T List. (as @ bs) T List
primrec Def primrec(n;b;c) == if n=0 b else c(n-1,primrec(n-1;b;c)) fi (recursive)
Thm* T:Type, n:, b:T, c:(nTT). primrec(n;b;c) T
eq_int Def i=j == if i=j true ; false fi
Thm* i,j:. (i=j)

Syntax:mklist(n;f) has structure: mklist(n; f)

About:
listconsconsnillist_indbool
bfalsebtrueifthenelseintnatural_numbersubtractint_eq
lambdaapplyfunctionrecursive_def_noticeuniversememberall
!abstraction

WhoCites Definitions MarkB generic Sections NuprlLIB Doc