mb event system 2 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def kind(e) == 1of(2of(2of(2of(2of(2of(2of(2of(es))))))))(e)

is mentioned by

Thm* es:ES, e:E, l:IdLnk, tg:Id.
Thm* kind(e) = rcv(ltg)
Thm* 
Thm* loc(e) = destination(l) & loc(sender(e)) = source(l)
[es-loc-rcv]
Def act(e) == act(kind(e))[es-act]
Def lnk(e) == lnk(kind(e))[es-lnk]
Def tag(e) == tag(kind(e))[es-tag]
Def isrcv(e) == isrcv(kind(e))[es-isrcv]

Try larger context: EventSystems IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

mb event system 2 Sections EventSystems Doc