WhoCites
Definitions
hol
list
1
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Who Cites hpair?
hpair
Def pair ==
x
:
'a
.
y
:
'b
. <
x
,
y
>
Thm*
'a
,
'b
:S. pair
(
'a
'b
hprod(
'a
;
'b
))
tlambda
Def
(
x
:
T
.
b
(
x
))(
x
) ==
b
(
x
)
Syntax:
pair
has structure:
hpair(
'a
;
'b
)
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
WhoCites
Definitions
hol
list
1
Sections
HOLlib
Doc