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

is mentioned by

Thm* 'a:S, P:(('a List)). (l:'a List. ||l|| = 0    P(l))  P(nil)	[length_eq_nil]
Thm* 'a:S, P:(('a List)), n:. Thm* (l:'a List. ||l|| = n+1    P(l)) Thm*  Thm* (l:'a List. ||l|| = n    (x:'a. P(cons(x; l))))	[length_eq_cons]
Thm* 'a:S, l:'a List, n:. Thm* ||l|| = n+1    (h:'a, l':'a List. ||l'|| = n   & l = cons(h; l'))	[length_cons_2]
Thm* 'a:S, l:'a List. ||l|| = 0    l = nil	[length_nil_2]
Thm* 'a:S, l:'a List, P:('a). every(P;l)  (n:. n<||l||  P(l[n]))	[every_el]
Thm* 'b,'a:S, l:'a List, f:('a'b). ||map(f;l)|| = ||l||	[length_map]
Thm* 'a:S, l1,l2:'a List. ||l1 @ l2|| = ||l1||+||l2||	[length_append_2]

In prior sections: list 1 hol list 1

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