Def i=j == if i=j true ; false fi

is mentioned by

Thm* Y(f,x. if x=0 1 else xf(x-1) fi)	[sfa_doc_ycomb_factorial_typing]
Thm* (f,x. if x=0 1 else xf(x-1) fi)  (k:. (k)(k+1))	[sfa_doc_factbody_polytyping]
Thm* f:().  Thm* (n:. f(n) = 0) Thm*  Thm* (n:. if f(n)=0 False else C:Prop{1}. C fi)  Prop{1}	[sfa_doc_predicativity_sample8]
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 i even == 0=(i rem 2)	[sfa_doc_even]
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]

In prior sections: bool 1 sqequal 1 int 2

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