Def firstn(n;as)
Def == Case of as
Def == Canil  nil
Def == Caa.as'  if 0<n [a / firstn(n-1;as')] else nil fi
Def (recursive)

is mentioned by

Thm* ll:(T List) List, n:||concat(ll)||. Thm* m:||ll||.  Thm* ||concat(firstn(m;ll))||n Thm* & n-||concat(firstn(m;ll))||<||ll[m]|| Thm* & concat(ll)[n] = ll[m][(n-||concat(firstn(m;ll))||)]	[select_concat]
Thm* n,m:. firstn(n;upto(m)) ~ if nm upto(n) else upto(m) fi	[firstn_upto]
Thm* f:(TopTop), n:, l:Top List. firstn(n;map(f;l)) ~ map(f;firstn(n;l))	[firstn_map]
Thm* L:Top List, n:. ||L||n  (firstn(n;L) ~ L)	[firstn_all]
Thm* L1,L2:Top List, n:(||L1||+1). firstn(n;L1 @ L2) ~ firstn(n;L1)	[firstn_append]
Thm* L:Top List. firstn(0;L) ~ nil	[first0]

In prior sections: list 1 mb list 1

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