Def as\[i]
Def == if i0 tl(as) else Case of as; nil  nil ; a'.as'  a'.as'\[i-1] fi
Def (recursive)

is mentioned by

Thm* a:T, as:T List, i:. 0<i  i||as||  (a.as)\[i] = a.as\[i-1]	[reject_cons_tl]
Thm* a:T, as:T List, i:. i0  (a.as)\[i] = as	[reject_cons_hd]

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