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* L1,L2:T List. L1  L2  (n:(||L2||+1). L1 = firstn(n;L2))	[firstn_is_iseg]
Thm* L:T List, n:{0...||L||}. (firstn(n;L) @ nth_tl(n;L)) = L	[append_firstn_lastn]

In prior sections: list 1

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