Definitions
hol
num
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Some definitions of interest.
nat
Def
== {
i
:
| 0
i
}
Thm*
Type
Thm*
S
tlambda
Def
(
x
:
T
.
b
(
x
))(
x
) ==
b
(
x
)
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Definitions
hol
num
Sections
HOLlib
Doc
== {i:
| 0
i } 
Type S
x:T. b(x))(x) == b(x) == {i:| 0i } Type Sx:T. b(x))(x) == b(x)
