Def ||as|| == Case of as; nil  0 ; a.as'  ||as'||+1  (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* 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* 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* P:(TProp), A,B:T List. Thm* A = B  (i:||A||. P(A[i]))  A = B  {x:T| P(x) } List	[list-eq-set-type]
Thm* n:. ||upto(n)|| ~ n	[length_upto]
Thm* r:, L:Top List. ||nth_tl(r;L)|| = if r<||L|| ||L||-r else 0 fi	[general_length_nth_tl]
Thm* f:Top, T:Type, L:T List, i:||L||. map(f;L)[i] ~ (f(L[i]))	[select-map]
Thm* f:Top, T:Type, L:T List. ||map(f;L)|| ~ ||L||	[length-map]
Thm* l:T List, i:||l||, j:i. last(l_interval(l;j;i)) = l[(i-1)]	[last_l_interval]
Thm* l:T List, i:||l||, j:i. hd(l_interval(l;j;i)) = l[j]	[hd_l_interval]
Thm* l:T List, i:||l||, j:(i+1), x:(i-j). l_interval(l;j;i)[x] = l[(j+x)]	[select_l_interval]
Thm* l:T List, i:||l||, j:(i+1). ||l_interval(l;j;i)|| = i-j	[length_l_interval]
Thm* f:(A), L:A List. 0<||L||  (aL.(xL.f(x)f(a)))	[maximal-in-list]
Def (x,yL.P(x;y)) == i:||L||, j:i. P(L[j];L[i])	[pairwise]

In prior sections: list 1 mb basic mb nat mb list 1 mb list 2

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