Nuprl - Some Definitions

	Who Cites mklist?

mklist	`Def 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: