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

is mentioned by

Def f{m..n} == if nm nil else f(m).f{(m+1)..n} fi  (recursive)	[listify]
Def as\[i] Def == if i0 tl(as) else Case of as; nil  nil ; a'.as'  a'.as'\[i-1] fi Def (recursive)	[reject]
Def firstn(n;as) Def == Case of as; nil  nil ; a.as'  if 0<n a.firstn(n-1;as') else nil fi Def (recursive)	[firstn]
Def nth_tl(n;as) == if n0 as else nth_tl(n-1;tl(as)) fi  (recursive)	[nth_tl]

In prior sections: bool 1 int 2

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