Definitions
hol
bool
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Some definitions of interest.
ball
Def
x
:
T
.
P
(
x
) ==
(
x
:
T
.
P
(
x
))
Thm*
T
:Type,
P
:(
T
). (
x
:
T
.
P
(
x
))
band
Def
p
q
== if
p
q
else false
fi
Thm*
p
,
q
:
. (
p
q
)
bimplies
Def
p
q
==
p
q
Thm*
p
,
q
:
.
p
q
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
bool
Sections
HOLlib
Doc