Definitions
num
thy
1
Sections
StandardLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Some definitions of interest.
assoced
Def
a
~
b
==
a
|
b
&
b
|
a
Thm*
a
,
b
:
. (
a
~
b
)
Prop
int_nzero
Def
== {
i
:
|
i
0 }
Thm*
Type
not
Def
A
==
A
False
Thm*
A
:Prop. (
A
)
Prop
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Definitions
num
thy
1
Sections
StandardLIB
Doc
a,b:
. (a ~ b) 
Prop
== {i:| i 
0 } Type
A == A 
FalseA:Prop. (A) Propa,b:. (a ~ b) Prop == {i:| i 0 } TypeA == A FalseA:Prop. (A) Prop
