Definitions
sqequal
1
Sections
StandardLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Some definitions of interest.
eq_int
Def
i
=
j
== if
i
=
j
true
; false
fi
Thm*
i
,
j
:
. (
i
=
j
)
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
sqequal
1
Sections
StandardLIB
Doc
j == if i=j
true ; false fi
i,j:
. (i=j) 
b T == 
a = b TA:Type, x,y:A. (x y) Propj == if i=j true ; false fii,j:. (i=j) b T == a = b TA:Type, x,y:A. (x y) Prop
