Definitions mb event system 5 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Some definitions of interest.
ma-doutDef M.dout(l,tg) == 1of(2of(M))(rcv(ltg))?Void
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'}
IdLnkDef IdLnk == IdId
Thm* IdLnk  Type
IdDef Id == Atom
Thm* Id  Type
fpfDef a:A fp-> B(a) == d:A Lista:{a:A| (a  d) }B(a)
Thm* A:Type, B:(AType). a:A fp-> B(a Type
pi1Def 1of(t) == t.1
Thm* A:Type, B:(AType), p:(a:AB(a)). 1of(p A

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

Definitions mb event system 5 Sections EventSystems Doc