WhoCites
Definitions
hol
list
2
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Who Cites head?
head
Def head(
l
) == hd(
l
)
Thm*
'a
:Type,
l
:
'a
List.
mt(
l
)
head(
l
)
'a
hd
Def
hd(
l
) == Case of
l
; nil
"?" ;
h
.
t
h
Thm*
A
:Type,
l
:
A
List. ||
l
||
1
hd(
l
)
A
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
WhoCites
Definitions
hol
list
2
Sections
HOLlib
Doc
'a:Type, l:'a List. 
mt(l) 
head(l) 
'a
"?" ; h.t hA:Type, l:A List. ||l||
1 hd(l) A'a:Type, l:'a List. mt(l) head(l) 'a "?" ; h.t hA:Type, l:A List. ||l||1 hd(l) A
