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
iff
Def
P
Q
== (
P
Q
) & (
P
Q
)
Thm*
A
,
B
:Prop. (
A
B
)
Prop
nat
Def
== {
i
:
| 0
i
}
Thm*
Type
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
Q == (P 
Q) & (P Q)A,B:Prop. (A B) Prop
== {i:| 0
i } Typea,b:. (a ~ b) Prop Q == (P Q) & (P Q)A,B:Prop. (A B) Prop == {i:| 0i } Type
