WhoCites Definitions int 2 Sections StandardLIB 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(b ; tf)
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 int 2 Sections StandardLIB Doc