Definitions
DiscrMathExt
Sections
NuprlLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
No other cites to report in DiscrMathExt
allst_implicit
Def
Q
(
x
) ==
x
:
A
st
P
(
x
).
Q
(
x
)
allst
Def
x
:
A
st
P
(
x
).
Q
(
x
) ==
x
:
A
.
P
(
x
)
Q
(
x
)
Syntax:
Q
(
x
)
has structure:
allst_implicit(
A
;
x
.
P
(
x
);
x
.
Q
(
x
))
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Definitions
DiscrMathExt
Sections
NuprlLIB
Doc
x:A st P(x). Q(x) x:A st P(x). Q(x) == x:A. P(x) 
Q(x) x:A st P(x). Q(x) x:A st P(x). Q(x) == x:A. P(x) Q(x)
