WhoCites Definitions LogicSupplement Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Who Cites ifthenelse?
ifthenelseDef  if b t else f fi == InjCase(btf)
Thm*  b:A:Type, p,q:A. if b p else q fi  A

Syntax:if b t else f fi has structure: ifthenelse(btf)

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

WhoCites Definitions LogicSupplement Sections DiscrMathExt Doc