WhoCites
Definitions
StandardLib
Sections
NuprlLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Who Cites unique
set?
unique_set
Def {!
x
:
T
|
P
(
x
)} == {
x
:
T
|
P
(
x
) & (
y
:
T
.
P
(
y
)
y
=
x
) }
Thm*
T
:Type,
P
:(
T
Prop). {!
x
:
T
|
P
(
x
)}
Type
Syntax:
{!
x
:
T
|
P
(
x
)}
has structure:
unique_set(
T
;
x
.
P
(
x
))
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
WhoCites
Definitions
StandardLib
Sections
NuprlLIB
Doc
y:T. P(y) 
y = x) }T:Type, P:(T
Prop). {!x:T | P(x)} 
Typey:T. P(y) y = x) }T:Type, P:(TProp). {!x:T | P(x)} Type
