WhoCites Definitions IteratedBinops Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
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 IteratedBinops Sections DiscrMathExt Doc