Who Cites res lambda?
res_lambda	Def res_lambda('a;'b;x.P(x);x.f(x)) == x:'a. if P(x) then f(x) else arb('b) fi
	Thm* 'a,'b:S, P:('a), f:('a'b). res_lambda('a;'b;x.P(x);x.f(x))  'a'b
arb	Def arb(T) == InjCase(lem(T); x. x, "uu")
	Thm* T:S. arb(T)  T
bif	Def bif(b; bx.x(bx); by.y(by)) == if b x(*) else y(x.x) fi
	Thm* A:Type, b:, x:(bA), y:((b)A). bif(b; bx.x(bx); by.y(by))  A
tlambda	Def (x:T. b(x))(x) == b(x)

Syntax:

res_lambda('a;'b;x.P(x);x.f(x))

has structure:

res_lambda('a; 'b; x.P(x); x.f(x))

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html