IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
The Derivation of Booleans - continued from Boolean
Def 
== Unit+Unit
where Unit is type with one value "
" (see Unit and Disjoint Union).
Def true
== inl()
Def false == inr()
Def if b
t else f fi == InjCase(b ; t; f)
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
