Nuprl - Some Definitions

bool	`Def == Unit+Unit` `Thm* Type`
eq_bool	`Def p=q == (pq) (pq)` `Thm* p,q:. p=q`
assert	`Def b == if b True else False fi` `Thm* b:. b Prop`
iff	`Def P Q == (P Q) & (P Q)` `Thm* (A B) Prop`
bnot	`Def b == if b false else true fi` `Thm* b:. b`
band	`Def pq == if p q else false fi` `Thm* p,q:. (pq)`
bor	`Def p q == if p true else q fi` `Thm* p,q:. (p q)`
ifthenelse	`Def if b t else f fi == dec(b ; t; f)` `Thm* b:, A:Type, p,q:A. if b p else q fi A`
rev_implies	`Def P Q == Q P` `Thm* (A B) Prop`
btrue	`Def true ==` `Thm* true`
bfalse	`Def false ==` `Thm* false`