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.
da-outlinksDef da-outlinks(da;i)
Def == mapfilter(k.da-outlink-f(da;k);k.has-src(i;k);fpf-dom-list(da))
Kind-deqDef KindDeq == union-deq(IdLnkId;Id;product-deq(IdLnk;Id;IdLnkDeq;IdDeq);IdDeq)
KndDef Knd == (IdLnkId)+Id
Thm* Knd  Type
IdLnkDef IdLnk == IdId
Thm* IdLnk  Type
IdDef Id == Atom
Thm* Id  Type
has-srcDef has-src(i;k) == isrcv(k)source(lnk(k)) = i
assertDef b == if b True else False fi
Thm* b:b  Prop
fpfDef a:A fp-> B(a) == d:A Lista:{a:A| (a  d) }B(a)
Thm* A:Type, B:(AType). a:A fp-> B(a Type
fpf-domDef x  dom(f) == deq-member(eq;x;1of(f))
isrcvDef isrcv(k) == isl(k)
Thm* k:Knd. isrcv(k 
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:
productproductlistboolifthenelseassertatomunionset
lambdaapplyfunctionuniversememberpropfalsetrueall
!abstraction
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Definitions mb event system 5 Sections EventSystems Doc