hol list 1 Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def rep_list('a;l) == <n:. if n<||l|| then l[n] else arb('a) fi ,||l||>

is mentioned by

Def abs_list == r:('a). @a:'a List. (r = rep_list('a;a))[habs_list]
Def rep_list == l:'a List. rep_list('a;l)[hrep_list]

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

hol list 1 Sections HOLlib Doc