Definitions
StandardLib
Sections
NuprlLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
NOTE:
"[C]
P
(%xm)"
is just a notation for
%xm
:XM.
P
(
%xm
)
No other cites to report in StandardLib
xmiddle
Def XM ==
P
:Prop. Dec(
P
)
Thm* XM{i}
Prop{i'}
decidable
Def
Dec(
P
) ==
P
P
Thm*
A
:Prop. Dec(
A
)
Prop
not
Def
A
==
A
False
Thm*
A
:Prop. (
A
)
Prop
Syntax:
XM
has structure:
xmiddle{i:l}
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Definitions
StandardLib
Sections
NuprlLIB
Doc