WhoCites
Definitions
StandardLib
Sections
NuprlLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
NOTE:
The "guard" operator, which is usually invisible, is used in some lemmas simply to guide matching heuristics, and has no semantic significance.
Who Cites guard?
guard
Def {
T
} ==
T
Thm*
T
:Type.
T
Type
Syntax:
T
has structure:
guard(
T
)
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
WhoCites
Definitions
StandardLib
Sections
NuprlLIB
Doc