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.
KndDef Knd == (IdLnkId)+Id
Thm* Knd  Type
ma-stateDef State(ds) == x:Idds(x)?Top
ma-valtypeDef ma-valtype(dak) == da(k)?Top
IdDef Id == Atom
Thm* Id  Type
kindcaseDef kindcase(k;a.f(a);l,t.g(l;t))
Def == if islocal(k) f(act(k)) else g(lnk(k);tag(k)) fi
Thm* B:Type, k:Knd, f:(IdB), g:(IdLnkIdB).
Thm* kindcase(k;a.f(a);l,t.g(l,t))  B
actofDef act(k) == outr(k)
Thm* k:Knd. islocal(k act(k Id
fpf-singleDef x : v == <[x],x.v>
islocalDef islocal(k) == isl(k)
Thm* k:Knd. islocal(k 

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

Definitions mb event system 5 Sections EventSystems Doc