mb event system 5 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
RankTheoremName
2Thm* da:k:Knd fp-> Type, i:Id. da-outlinks(da;i (IdLnkIdType) List[da-outlinks_wf]
cites the following:
1Thm* T:Type, P:(T), T':Type, f:({x:TP(x) }T'), L:T List.
Thm* mapfilter(f;P;L T' List
[mapfilter_wf]
0Thm* i:Id, k:Knd. has-src(i;k isrcv(k) & source(lnk(k)) = i[assert-has-src]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
mb event system 5 Sections EventSystems Doc