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