Definitions mb event system 4 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Some definitions of interest.
da-outlinksDef da-outlinks(da;i)
Def == mapfilter(k.da-outlink-f(da;k);k.has-src(i;k);fpf-dom-list(da))
IdLnkDef IdLnk == IdId
Thm* IdLnk  Type
IdDef Id == Atom
Thm* Id  Type
fpf-emptyDef  == <nil,x.>
l_memberDef (x  l) == i:i<||l|| & x = l[i T
Thm* T:Type, x:Tl:T List. (x  l Prop
mapfilterDef mapfilter(f;P;L) == map(f;filter(P;L))
Thm* T:Type, P:(T), T':Type, f:({x:TP(x) }T'), L:T List.
Thm* mapfilter(f;P;L T' List

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

Definitions mb event system 4 Sections EventSystems Doc