Def f{m..n} == if nm nil else f(m).f{(m+1)..n} fi  (recursive)

is mentioned by

Thm* n:, f:(nT), i:n. (f{n})[i] = f(i)	[select_listify_id]
Thm* as:T List. (i:||as||. as[i]){||as||} = as	[listify_select_id]
Thm* m,n:, f:({m..n}T). n<m  ||f{m..n}|| = n-m	[listify_length]

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