Def  if b t else f fi == InjCase(b; . t, f)

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]
Def  (s1 @(m) s2)(x) == if xm s1(x) else s2(x) fi	[hanoi_seq_join]
Def  (f {to n}  f' {to n'})(i) == if in f(i) else f'(i) fi	[hanoi_extend]
Def  permute(p to r ; q to s)(u) == if u=p r ; u=q s else otherPeg(r; s) fi	[hanoi_peg_perm]

In prior sections: bool 1 int 2

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