WhoCites Definitions LogicSupplement Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
This operator coercing a to a Prop is normally invisible since it is pretty obvious when it is needed.

Who Cites assert?
assertDef  b == if b True else False fi
Thm*  b:b  Prop

Syntax:b has structure: assert(b)

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

WhoCites Definitions LogicSupplement Sections DiscrMathExt Doc