Def nth_tl(n;as) == if n0 as else nth_tl(n-1;tl(as)) fi  (recursive)

is mentioned by

Thm* m:, L:T List. m<||L||  (nth_tl(m;L) ~ [L[m] / nth_tl(1+m;L)])	[nth_tl_decomp]
Thm* L:T List, n:{0...||L||}. (firstn(n;L) @ nth_tl(n;L)) = L	[append_firstn_lastn]

In prior sections: list 1

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