Def mklist(n;f) == primrec(n;nil;i,l. l @ [(f(i))])

is mentioned by

Thm* n:, f:(nT), i:n. mklist(n;f)[i] = f(i)	[mklist_select]
Thm* n:, f:(nT). ||mklist(n;f)|| = n	[mklist_length]

Try larger context: MarkB generic IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html