WhoCites Definitions mb tree Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
NOTE: 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 mb tree Sections MarkB generic Doc