Def Y(f) == (x.f(x(x)))(x.f(x(x)))

is mentioned by

Def R^n == if n=0 x,y. x = y  T else x,y. z:T. (x R z) & (z R^n-1 y) fi Def (recursive)	[rel_exp]
Def primrec(n;b;c) == if n=0 b else c(n-1,primrec(n-1;b;c)) fi  (recursive)	[primrec]

In prior sections: list 1

Try larger context: MarkB generic IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html