Definitions
hol
min
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Some definitions of interest.
hfun
Def
'a
'b
==
'a
'b
Thm*
'a
,
'b
:S. (
'a
'b
)
S
label
Def
t
...$L ==
t
stype
Def
S == {
T
:Type|
x
:
T
. True }
Thm*
S
Type{2}
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Definitions
hol
min
Sections
HOLlib
Doc
'b == 'a'b
'a,'b:S. ('a 'b) 
S
x:T. True } Type{2} 'b == 'a'b'a,'b:S. ('a 'b) Sx:T. True } Type{2}
