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

is mentioned by

Def upto(n) == if n=0 nil else upto(n-1) @ [(n-1)] fi  (recursive)	[upto]
Def mu(f) == if f(0) 0 else mu(x.f(x+1))+1 fi  (recursive)	[mu]

In prior sections: list 1 mb nat mb list 1 num thy 1

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