Definitions mb event system 3 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Some definitions of interest.
w-MsgDef Msg == Msg(w.M)
w-actionDef Action(i) == action(w-action-dec(w.TA;w.M;i))
worldDef World
Def == T:IdIdType
Def == TA:IdIdType
Def == M:IdLnkIdType
Def == (i:Id(x:IdT(i,x)))(i:Idaction(w-action-dec(TA;M;i)))
Def == (i:Id({m:Msg(M)| source(mlnk(m)) = i } List))Top
Thm* World  Type{i'}
IdLnkDef IdLnk == IdId
Thm* IdLnk  Type
w-queueDef queue(l;t) == nth_tl(||rcvs(l;t)||;snds(l;t))
w-isrcvlDef isrcv(l;a) == isnull(a)isrcv(kind(a))lnk(kind(a)) = l
IdDef Id == Atom
Thm* Id  Type
assertDef b == if b True else False fi
Thm* b:b  Prop
geDef ij == ji
Thm* i,j:. (ij Prop
isrcvDef isrcv(k) == isl(k)
Thm* k:Knd. isrcv(k 
lengthDef ||as|| == Case of as; nil  0 ; a.as'  ||as'||+1  (recursive)
Thm* A:Type, l:A List. ||l||  
Thm* ||nil||  
w-msgDef msg(a) == msg(lnk(kind(a));tag(kind(a));val(a))
lnkDef lnk(k) == 1of(outl(k))
Thm* k:Knd. isrcv(k lnk(k IdLnk
natDef  == {i:| 0i }
Thm*   Type
notDef A == A  False
Thm* A:Prop. (A Prop
w-aDef a(i;t) == 1of(2of(2of(2of(2of(w)))))(i,t)
w-isnullDef isnull(a) == isl(a)
w-kindDef kind(a) == 1of(outr(a))

About:
productproductlistnillist_indbool
ifthenelseassertintnatural_numberaddatomsetapplyfunction
recursive_def_noticeuniverseequalmembertoppropimpliesfalsetrueall
!abstraction
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Definitions mb event system 3 Sections EventSystems Doc