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

is mentioned by

Thm* n,m:. firstn(n;upto(m)) ~ if nm upto(n) else upto(m) fi	[firstn_upto]
Thm* r:, L:Top List. ||nth_tl(r;L)|| = if r<||L|| ||L||-r else 0 fi	[general_length_nth_tl]
Def upto(n) == if n=0 nil else upto(n-1) @ [(n-1)] fi  (recursive)	[upto]
Def mu(f) == if f(0) 0 else mu(x.f(x+1))+1 fi  (recursive)	[mu]

In prior sections: bool 1 mb nat mb list 2 int 2 list 1 mb list 1 num thy 1

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