Def  == {i:| 0i }

is mentioned by

Thm* 'a:S. iso_pair('a List;('a);is_list_rep;rep_list;abs_list)	[list_iso]
Thm* 'a:S, n:, l:'a List. n<||l||  el(n,l) = l[n]	[hel_nuprl]
Thm* it_sum(nil) = 0 Thm* & (l: List. mt(l)  it_sum(l) = head(l)+it_sum(tl(l))) Thm* & (x:, l: List. it_sum(cons(x; l)) = x+it_sum(l))	[it_sum_def]
Thm* l: List. it_sum(l)	[it_sum_wf]
Thm* 'a:S, l:'a List. rep_list('a;l)  ('a)	[rep_list_wf]
Thm* 'a:Type, l:'a List. ||l||	[length_wf_nat]
Def el == n:. l:'a List. if n=0 then hd(l) else el(n-1,tl(l)) fi  Def (recursive)	[hel]
Def it_sum == l: List. it_sum(l)	[hit_sum]
Def abs_list == r:('a). @a:'a List. (r = rep_list('a;a))	[habs_list]
Def is_list_rep Def == r:('a). f:'a Def == r:('a). n: Def == r:('a). (r Def == r:('a). = <m:. if m<n then f(m) else @x:'a. true fi ,n>)	[his_list_rep]
Def rep_list('a;l) == <n:. if n<||l|| then l[n] else arb('a) fi ,||l||>	[rep_list]

In prior sections: int 1 bool 1 int 2 list 1 hol num hol prim rec hol arithmetic 1 hol min

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