Definitions
hol
prim
rec
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
nat
Def
== {
i
:
| 0
i
}
Thm*
Type
Thm*
S
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
prim
rec
Sections
HOLlib
Doc
'b == 'a'b
'a,'b:S. ('a 'b) 
S
== {i:
| 0
i } Type S
x:T. True } Type{2} 'b == 'a'b'a,'b:S. ('a 'b) S == {i:| 0i } Type Sx:T. True } Type{2}
