WhoCites
Definitions
NuprlPrimitives
Sections
NuprlLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Who Cites int
nzero?
int_nzero
Def
== {
i
:
|
i
0 }
Thm*
Type
nequal
Def
a
b
T
==
a
=
b
T
Thm*
A
:Type,
x
,
y
:
A
. (
x
y
)
Prop
not
Def
A
==
A
False
Thm*
A
:Prop. (
A
)
Prop
Syntax:
has structure:
int_nzero
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
WhoCites
Definitions
NuprlPrimitives
Sections
NuprlLIB
Doc