Def f(x)?z == if x  dom(f) f(x) else z fi

is mentioned by

Thm* x:Id, k:Knd, ds:x:Id fp-> Type, da:a:Knd fp-> Type, Thm* f:(State(ds)ma-valtype(da; k)ds(x)?Void). Thm* ma-single-effect(ds; da; k; x; f)  MsgA	[ma-single-effect_wf]
Thm* eq:EqDecider(A), f,g:a:A fp-> Top, x:A, z:Top. Thm* f  g(x)?z ~ if x  dom(f) f(x)?z else g(x)?z fi	[fpf-join-cap-sq]
Thm* eq:EqDecider(X), f,g:x:X fp-> Type, x:X. f  g  (f(x)?Void r g(x)?T)	[subtype-fpf-cap-void]
Thm* eq:EqDecider(A), ds:x:A fp-> Type, x:A. ds(x)?Void r ds(x)?Top	[fpf-cap-void-subtype]
Thm* eq:EqDecider(X), f,g:x:X fp-> Type, x:X. g  f  (f(x)?T r g(x)?Top)	[subtype-fpf-cap-top]
Thm* eq:EqDecider(X), f,g:x:X fp-> Type. g  f  (x:X. f(x)?Top r g(x)?Top)	[subtype-fpf-cap]
Thm* A:Type, f:a:A fp-> Type, eq:EqDecider(A), x:A, z:Type. f(x)?z  Type	[fpf-cap-wf-univ]

In prior sections: mb event system 4

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