Definitions mb event system 7 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Some definitions of interest.
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'}
KndDef Knd == (IdLnkId)+Id
Thm* Knd  Type
IdDef Id == Atom
Thm* Id  Type
recognizer1Def recognizer1(loc;T;A;P;k;i;r;x)
Def == if loc = i
Def == if [r :  initially r = false
Def == if [only members of [k] affect r :
Def == if [ma-single-effect1(r;;x;A;k;T;r,x,vP(x,v r)]
Def == else nil fi
Thm* loc:Id, T,A:Type, P:(AT), k:Knd, i,r,x:Id.
Thm* A  T  x = r  recognizer1(loc;T;A;P;k;i;r;x MsgA List
notDef A == A  False
Thm* A:Prop. (A Prop

About:
productproductlistconsnilboolbfalse
ifthenelsevoidatomunionlambdaapply
functionuniverseequalmembertoppropimpliesfalse
all!abstraction
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Definitions mb event system 7 Sections EventSystems Doc