Nuprl Definition : compose-fpf

compose-fpf(a;b;f) ==  <mapfilter(λx.outl(a x);λx.isl(a x);fpf-domain(f)), (snd(f)) o b>



Definitions occuring in Statement :  fpf-domain: fpf-domain(f),  mapfilter: mapfilter(f;P;L),  compose: f o g,  outl: outl(x),  isl: isl(x),  pi2: snd(t),  apply: f a,  lambda: λx.A[x],  pair: <a, b>
FDL editor aliases :  compose-fpf
compose-fpf(a;b;f)  ==    <mapfilter(\mlambda{}x.outl(a  x);\mlambda{}x.isl(a  x);fpf-domain(f)),  (snd(f))  o  b>



Date html generated: 2015_07_17-AM-11_11_40
Last ObjectModification: 2012_02_25-AM-11_11_43

Home Index