Definitions mb event system 6 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Some definitions of interest.
ma-frame-compatibleDef ma-frame-compatible(AB)
Def == kx:(KndId). 
Def == (kx  dom(1of(2of(2of(2of(2of(A))))))
Def == (
Def == (2of(kx dom(1of(2of(2of(2of(2of(2of(2of(A))))))))
Def == (
Def == (2of(kx dom(1of(2of(2of(2of(2of(2of(2of(B))))))))
Def == (
Def == (deq-member(KindDeq;1of(kx);1of(2of(2of(2of(2of(2of(2of(
Def == (deq-member(KindDeq;1of(kx);1of(B)))))))(2of(kx))))
Def == & (kx  dom(1of(2of(2of(2of(2of(B))))))
Def == & (
Def == & (2of(kx dom(1of(2of(2of(2of(2of(2of(2of(B))))))))
Def == & (
Def == & (2of(kx dom(1of(2of(2of(2of(2of(2of(2of(A))))))))
Def == & (
Def == & (deq-member(KindDeq;1of(kx);1of(2of(2of(2of(2of(2of(2of(
Def == & (deq-member(KindDeq;1of(kx);1of(A)))))))(2of(kx))))
msgaDef MsgA
Def == ds:x:Id fp-> Type
Def == da:a:Knd fp-> Type
Def == x:Id fp-> ds(x)?Voida:Id fp-> State(ds)ma-valtype(da; locl(a))Prop
Def == kx:KndId fp-> State(ds)ma-valtype(da; 1of(kx))ds(2of(kx))?Void
Def == kl:KndIdLnk fp-> (tg:Id
Def == kl:KndIdLnk fp-> (State(ds)ma-valtype(da; 1of(kl))
Def == kl:KndIdLnk fp-> ((da(rcv(2of(kl); tg))?Void List)) List
Def == x:Id fp-> Knd Listltg:IdLnkId fp-> Knd ListTop
Thm* MsgA  Type{i'}

About:
productproductlistvoidfunctionuniversemember
toppropimpliesandall!abstraction
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Definitions mb event system 6 Sections EventSystems Doc