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

is mentioned by

Thm* as:T List, n:{0...||as||}, i:(||as||-n). nth_tl(n;as)[i] = as[(i+n)]	[select_nth_tl]
Thm* as:A List, n:{0...||as||}. ||nth_tl(n;as)|| = ||as||-n	[length_nth_tl]
Def l[i] == hd(nth_tl(i;l))	[select]
Def as[m..n] == firstn(n-m;nth_tl(m;as))	[segment]

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