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

is mentioned by

Thm* eq:EqDecider(A), x,y:A, v,z:Top. Thm* x : v(y)?z ~ if eqof(eq)(x,y) v else z fi	[fpf-cap-single]
Thm* eq:EqDecider(A), f:a:A fp-> Top, g:Top, x:A. Thm* f  g(x) ~ if x  dom(f) f(x) else g(x) fi	[fpf-join-ap-sq]
Def M.send(k;l;s;v;ms;i) Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> ms Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> = Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> if source(l) = i Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> if concat(map(tgf. Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> if map(x. Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> if <1of(tgf),x>;2of(tgf) Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> if <1of(tgf),x>;(s Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> if <1of(tgf),x>;,v));L)) Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> else nil fi Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==>  (tg:Id Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==>  (if source(l) = i Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==>  (if M.da(rcv(l; tg)) Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==>  (else Top fi) List	[ma-send]

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

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