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

is mentioned by

Thm* Y(f,x. if x=0 1 else xf(x-1) fi)	[sfa_doc_ycomb_factorial_typing]
Def a list xs == Case of xs; nil  False ; x.ys  x = a  A  a list ys Def (recursive)	[sfa_doc_inlist]
Def i steps of e from a == if i=0 a else e(i-1 steps of e from a) fi Def (recursive)	[sfa_doc_sequence_rel]
Def Reverse(e) Def == Case of e Def == CaInj(x)  Inj(x) Def == CaCons(s1;s2)  Cons(Reverse(s2);Reverse(s1)) Def (recursive)	[sfa_doc_sexpr_reverse]
Def Size(s) == Case of s :  Inj(x)  1 ; Cons(s1;s2)  Size(s1)+Size(s2) Def (recursive)	[sfa_doc_sexpr_size]
Def  u in X: A^n. P(u) Def == n = 1   & P(X)  n2 & (X/a,rest. P(a)  ( u in rest: A^(n-1). P(u))) Def (recursive)	[sfa_doc_ntuple_contains]
Def A^n == if n=0 Unit ; n=1 A else A(A^(n-1)) fi  (recursive)	[sfa_doc_ntuple]
Def x! == if x=0 1 else x(x-2)! fi  (recursive)	[sfa_doc_factorial2]
Def x! == if x=0 1 else x(x-1)! fi  (recursive)	[sfa_doc_factorial]
Def mu(f) == if f(0) 0 else 1+mu(x.f(1+x)) fi  (recursive)	[kleene_minimize]

In prior sections: list 1

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