Def ||as|| == Case of as; nil  0 ; a.as'  ||as'||+1  (recursive)

is mentioned by

Thm* 'a:S, n:, l:'a List. n<||l||  el(n,l) = l[n]	[hel_nuprl]
Def length == l:'a List. ||l||	[hlength]
Def rep_list('a;l) == <n:. if n<||l|| then l[n] else arb('a) fi ,||l||>	[rep_list]

In prior sections: list 1

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