Nuprl - Some Definitions

b2i	`Def b2i(b) == if b 1 else 0 fi` `Thm* b:. b2i(b)`
function_prim	`Def x:AB(x) == PRIMITIVE {Total functions from A: x.b(x) such that b(x) B(x) for x A }`
bool	`Def == Unit+Unit` `Thm* Type`
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`