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

is mentioned by

Thm* n:, as:A List(n). ||as|| = n	[list_n_properties]
Thm* as:T List. (i:||as||. as[i]){||as||} = as	[listify_select_id]
Thm* m,n:, f:({m..n}T). n<m  ||f{m..n}|| = n-m	[listify_length]
Thm* f:(AB), as:A List, n:||as||. map(f;as)[n] = f(as[n])	[map_select]
Thm* a:T, as:T List, i:. 0<i  i||as||  (a.as)\[i] = a.as\[i-1]	[reject_cons_tl]
Thm* as:T List, n:{0...||as||}, i:n. firstn(n;as)[i] = as[i]	[select_firstn]
Thm* as:T List, n:{0...||as||}, i:(||as||-n). nth_tl(n;as)[i] = as[(i+n)]	[select_nth_tl]
Thm* as:A List, n:(||as||-1). tl(as)[n] = as[(n+1)]	[select_tl]
Thm* as,bs:T List, i:||as||. (as @ bs)[i] = as[i]	[select_append_front]
Thm* as,bs:T List, i:{||as||..(||as||+||bs||)}. (as @ bs)[i] = bs[(i-||as||)]	[select_append_back]
Thm* a:T, as:T List, i:. 0<i  i||as||  (a.as)[i] = as[(i-1)]	[select_cons_tl]
Thm* A:Type, l:A List, n:. 0n  n<||l||  l[n]  A	[select_wf]
Thm* as:T List, i:{0...||as||}, j:{i...||as||}. ||as[i..j]|| = j-i	[length_segment]
Thm* as:A List, n:{0...||as||}. ||firstn(n;as)|| = n	[length_firstn]
Thm* as:A List, n:{0...||as||}. ||nth_tl(n;as)|| = ||as||-n	[length_nth_tl]
Thm* l:A List. ||l||1  ||tl(l)|| = ||l||-1	[length_tl]
Thm* A:Type, l:A List. ||l||1  hd(l)  A	[hd_wf]
Thm* f:(AB), as:A List. ||map(f;as)|| = ||as||	[map_length]
Thm* as:A List. as = nil  ||as|| = 0	[length_of_null_list]
Thm* as:A List. as = nil  ||as||1	[length_of_not_nil]
Thm* as,bs:T List. ||as @ bs|| = ||as||+||bs||	[length_append]
Thm* l:A List. l = nil  ||l||1	[pos_length]
Thm* l:A List. ||l||0	[non_neg_length]
Thm* ||nil|| = 0	[length_nil]
Thm* a:A, as:A List. ||a.as|| = ||as||+1	[length_cons]
Def A List(n) == {x:(A List)| ||x|| = n }	[list_n]

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