Definitions hol list 1 Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Some definitions of interest.
helDef el == n:l:'a List. if n=0 then hd(l) else el(n-1,tl(l)) fi 
Def (recursive)
Thm* 'a:S. el  (hnum  hlist('a 'a)
hfunDef 'a  'b == 'a'b
Thm* 'a,'b:S. ('a  'b S
hlistDef hlist('a) == 'a List
Thm* 'a:S. hlist('a S
natDef  == {i:| 0i }
Thm*   Type
Thm*   S
stypeDef S == {T:Type| x:T. True }
Thm* S  Type{2}
tlambdaDef (x:Tb(x))(x) == b(x)

About:
listintnatural_numbersubtractsetapplyfunction
recursive_def_noticeuniversemembertrueallexists
!abstraction
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Definitions hol list 1 Sections HOLlib Doc