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

is mentioned by

Thm* n:, f:(n), m:n. Thm* sum(f(x) | x < n) = f(m)+sum(if x=m 0 else f(x) fi | x < n)	[isolate_summand]
Thm* k:, f,g:(k), p:(k). Thm* sum(if p(i) f(i)+g(i) else f(i) fi | i < k) Thm* = Thm* sum(f(i) | i < k)+sum(if p(i) g(i) else 0 fi | i < k)	[sum-ite]
Def search(k;P) == primrec(k;0;i,j. if 0<j j ; P(i) i+1 else 0 fi)	[search]
Def (i, j)(x) == if x=i j ; x=j i else x fi	[flip]
Def R^n == if n=0 x,y. x = y  T else x,y. z:T. (x R z) & (z R^n-1 y) fi Def (recursive)	[rel_exp]
Def f[n:=x](i) == if i=n x else f(i) fi	[fappend]
Def primrec(n;b;c) == if n=0 b else c(n-1,primrec(n-1;b;c)) fi  (recursive)	[primrec]

In prior sections: bool 1 int 2 list 1

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