Definitions
DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Some definitions of interest.
nat
Def
== {
i
:
| 0
i
}
Thm*
Type
nequal
Def
a
b
T
==
a
=
b
T
Thm*
A
:Type,
x
,
y
:
A
. (
x
y
)
Prop
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Definitions
DiscreteMath
Sections
DiscrMathExt
Doc
== {i:
| 0
i } 
Type
b T == 
a = b T
A:Type, x,y:A. (x y) Prop == {i:| 0i } Type b T == a = b TA:Type, x,y:A. (x y) Prop
