WhoCites Definitions int 1 Sections StandardLIB 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?
guardDef {T} == T
Thm* T:Type. T  Type

Syntax:T has structure: guard(T)

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

WhoCites Definitions int 1 Sections StandardLIB Doc