mb event system 5 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def x  dom(f) == deq-member(eq;x;1of(f))

is mentioned by

Thm* da:k:Knd fp-> Type, k:{k:Knd| k  dom(da) & isrcv(k) }.
Thm* da-outlink-f(da;k IdLnkIdType
[da-outlink-f_wf]
Thm* eq:EqDecider(A), f,g:a:A fp-> Top, x:Az:Top.
Thm* f  g(x)?z ~ if x  dom(f) f(x)?z else g(x)?z fi
[fpf-join-cap-sq]
Thm* B,C:(AType), eq:EqDecider(A), f:a:A fp-> B(a), g:a:A fp-> C(a), x:A.
Thm* x  dom(f f  g(x) = f(x B(x)
[fpf-join-ap-left]
Thm* B:(AType), eq:EqDecider(A), f,g:a:A fp-> B(a), x:A.
Thm* x  dom(f  g f  g(x) = if x  dom(f) f(x) else g(x) fi  B(x)
[fpf-join-ap]
Thm* A:Type, B:(AType), f:a:A fp-> B(a), eq:EqDecider(A), x:A,
Thm* P:(a:{a:Aa  dom(f) }B(a)Prop). z != f(x) ==> P(x,z Prop
[fpf-val_wf]

In prior sections: mb event system 3 mb event system 4

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

mb event system 5 Sections EventSystems Doc