Def ||as|| == Case of as; nil  0 ; a.as'  ||as'||+1  (recursive)

is mentioned by

Thm* as:T1 List, bs:T2 List. ||as|| = ||bs||    unzip(zip(as;bs)) = <as,bs>	[unzip_zip]
Thm* as:T1 List, bs:T2 List. ||as|| = ||bs||    ||zip(as;bs)|| = ||as||	[length_zip]
Thm* as:T1 List, bs:T2 List, i:. Thm* i<||zip(as;bs)||  zip(as;bs)[i] = <as[i],bs[i]>	[select_zip]
Thm* as:T1 List, bs:T2 List. ||zip(as;bs)||||as|| & ||zip(as;bs)||||bs||	[zip_length]
Thm* l1,l2:T List. l1  l2  ||l1||||l2||	[iseg_length]
Thm* l1,l2:T List. l1  l2  ||l1||||l2|| & (i:. i<||l1||  l1[i] = l2[i])	[iseg_select]
Thm* L1,L2:T List. L1  L2  (n:(||L2||+1). L1 = firstn(n;L2))	[firstn_is_iseg]
Thm* l:A List. ||l||1	[listp_properties]
Thm* L:T List, i,j:||L||. i<j  [L[i]; L[j]]  L	[sublist_pair]
Thm* L1,L2:T List. L1  L2  ||L1|| = ||L2||    L1 = L2	[proper_sublist_length]
Thm* L1,L2:T List. L1  L2  ||L1||||L2||	[length_sublist]
Thm* L:T List, i:||L||. (L[i]  L)	[select_member]
Thm* as:T List, x:T. 0<||as||  (x  tl(as))  (x  as)	[member_tl]
Thm* n:, f:(nT). ||mklist(n;f)|| = n	[mklist_length]
Thm* z:T List. ||z|| = 2    z = [z[0]; z[1]]	[list_2_decomp]
Thm* f:(AB), as:A List. ||map(f;as)|| = ||as||	[map_length_nat]
Thm* L:T List. 0<||L||  (x:T, L':T List. L = (L' @ [x]))	[list_decomp_reverse]
Thm* a:T List, f,g:(TT'). Thm* (i:. i<||a||  f(a[i]) = g(a[i]))  map(f;a) = map(g;a)	[map_equal]
Thm* a,b:T List. ||a|| = ||b||    (i:. i<||a||  a[i] = b[i])  a = b	[list_extensionality]
Thm* m:, L:T List. m<||L||  (nth_tl(m;L) ~ [L[m] / nth_tl(1+m;L)])	[nth_tl_decomp]
Thm* L:T List. 0<||L||  (L ~ [hd(L) / tl(L)])	[list_decomp]
Thm* l:T List. ||l|| = 0    l = nil	[length_zero]
Thm* L:T List. L = nil  0<||L||	[non_nil_length]
Thm* L:T List, P:(||L||Prop). Thm* (x:||L||. Dec(P(x))) Thm*  Thm* (i,j:||L||. P(i)  i<j  P(j)) Thm*  Thm* (L_1,L_2:T List. L = (L_1 @ L_2) & (i:||L||. P(i)  ||L_1||i))	[append_split2]
Thm* L:T List, n:{0...||L||}. (firstn(n;L) @ nth_tl(n;L)) = L	[append_firstn_lastn]
Def no_repeats(T;l) == i,j:. i<||l||  j<||l||  i = j  l[i] = l[j]  T	[no_repeats]
Def A List == {l:(A List)| (0<||l||) }	[listp]
Def L1  L2 Def == f:(||L1||||L2||).  Def == increasing(f;||L1||) & (j:||L1||. L1[j] = L2[(f(j))]  T)	[sublist]
Def last(L) == L[(||L||-1)]	[last]
Def (x  l) == i:. i<||l|| & x = l[i]  T	[l_member]

In prior sections: list 1 mb basic mb nat

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