Def el == n:. l:'a List. if n=0 then hd(l) else el(n-1,tl(l)) fi 
Def (recursive)

is mentioned by

Thm* 'a:S, n:, l:'a List. n<||l||  el(n,l) = l[n]

[hel_nuprl]

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