Nuprl - Some Definitions

lt_int	`Def i < z j == if i < j true ; false fi` `Thm* i,j:. i < z j`
bnot	`Def b == if b false else true fi` `Thm* b:. b`
bool	`Def == Unit+Unit` `Thm* Type`
bfalse	`Def false ==` `Thm* false`
btrue	`Def true ==` `Thm* true`
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`