NuprlPrimitives Sections NuprlLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Subtypes by Comprehension - sometimes called "set types"

{x:AB(x) } is the subtype of A restricted to the Property B(x) (x  A).

It is the type of a  A such that B(a).

Note that "a  {x:AB(x) }" is not equivalent to "B(a)", since "B(a)" can be assigned a meaning for any a  A, but "a  {x:AB(x) }" is not assigned a meaning unless it is true, i.e., when "B(a)" is true.

See Polymorphism, Equality, Types and Guarded Types.

(Feb 2001 - sfa )

About:
member
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

NuprlPrimitives Sections NuprlLIB Doc