Nuprl - Some Definitions

eq_int	`Def i=j == if i=jtrue; false fi` `Thm* i,j:. i=j`
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`
function_prim	`Def x:AB(x) == PRIMITIVE {Total functions from A: x.b(x) such that b(x) B(x) for x A }`
nequal	`Def abT == a = b T` `Thm* x,y:A. xy Prop`
bfalse	`Def false ==` `Thm* false`
btrue	`Def true ==` `Thm* true`
not	`Def A == A False` `Thm* (A) Prop`