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

is mentioned by

Def  n^k == if k=0 1 else n(n^(k-1)) fi  (recursive)	[exponentiation]
Def  HanoiSTD(n disks; from: p; to: q; indexing from: a) Def  == if n=0 <a,x,i. whatever> Def  == else HanoiSTD(n-1 disks; from: p; to: otherPeg(p; q); indexing from: a) Def  == else /m,s1. Def  == else HanoiSTD(n-1 disks; from: otherPeg(p; q); to: q; indexing from: m Def  == else HanoiSTD(+1) Def  == else /z,s2. <z,HanoiHelper(n; s1; i.p; s2; i.q)/r1,r2. r1 @(m) r2> fi Def  (recursive)	[hanoi_sol2_ala_generalPROG]

In prior sections: bool 1 int 2

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