Def tl(l) == Case of l; nil  nil ; h.t  t

is mentioned by

Thm* as:A List, n:(||as||-1). tl(as)[n] = as[(n+1)]	[select_tl]
Thm* l:A List. ||l||1  ||tl(l)|| = ||l||-1	[length_tl]
Def as\[i] Def == if i0 tl(as) else Case of as; nil  nil ; a'.as'  a'.as'\[i-1] fi Def (recursive)	[reject]
Def nth_tl(n;as) == if n0 as else nth_tl(n-1;tl(as)) fi  (recursive)	[nth_tl]

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