Definitions
hol
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Some definitions of interest.
arb
Def
arb(
T
) == InjCase(lem(
T
);
x
.
x
, "uu")
Thm*
T
:S. arb(
T
)
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
Sections
HOLlib
Doc
T:S. arb(T) 
T
x:T. True } Type{2}T:S. arb(T) Tx:T. True } Type{2}
