Def upto(n) == if n=0 nil else upto(n-1) @ [(n-1)] fi  (recursive)

is mentioned by

Thm* f:((T List)), t,t':. Thm* t<t'  concat(map(f;upto(t))) @ (f(t))  concat(map(f;upto(t')))	[concat_map_upto]
Thm* n,m:. firstn(n;upto(m)) ~ if nm upto(n) else upto(m) fi	[firstn_upto]
Thm* t',m:, T:Type, f:(T), P:(T). Thm* m+1||filter(P;map(f;upto(t')))|| Thm*  Thm* (t:. P(f(t)) & ||filter(P;map(f;upto(t)))|| = m  )	[filter_map_upto2]
Thm* i,j:. Thm* i<j Thm*  Thm* (f:(T), P:(T). Thm* (P(f(i))  ||filter(P;map(f;upto(i)))||<||filter(P;map(f;upto(j)))||)	[filter_map_upto]
Thm* n:, x,y:n. x before y  upto(n)  x<y	[before-upto]
Thm* n,i:. i<n  (i  upto(n))	[member_upto2]
Thm* n,i:. (i  upto(n))  i<n	[member_upto]
Thm* m:, n:m. upto(m)[n] = n	[select_upto]
Thm* i,j:. ij  upto(i)  upto(j)	[upto_iseg]
Thm* m:, n:(m+1). upto(m) ~ (upto(n) @ map(x.x+n;upto(m-n)))	[upto_decomp]
Thm* n:. ||upto(n)|| ~ n	[length_upto]

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