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

is mentioned by

Def (L o f) == mklist(||L||;i.L[(f(i))])

[permute_list]

In prior sections: mb list 1

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