dfpX
>>= dfpY ==
  let Abg,S,s,F = dfpX
  in <B
     , S? 
 bag(a:A 
 (fst(snd((dfpY a)))))
     , <inl s , {}>
     , 
s,m.evalall(bind-df-next(F;dfpY;s;m))>  
Definitions occuring in Statement : 
bind-df-next: bind-df-next(F;dfpY;s;m), 
spreadn: spread4, 
pi1: fst(t), 
pi2: snd(t), 
unit: Unit, 
apply: f a, 
lambda:
x.A[x], 
pair: <a, b>, 
product: x:A 
 B[x], 
inl: inl x , 
union: left + right, 
empty-bag: {}, 
bag: bag(T), 
evalall: evalall(t)
Definitions : 
spreadn: spread4, 
union: left + right, 
unit: Unit, 
bag: bag(T), 
product: x:A 
 B[x], 
pi1: fst(t), 
pi2: snd(t), 
apply: f a, 
pair: <a, b>, 
inl: inl x , 
empty-bag: {}, 
lambda:
x.A[x], 
evalall: evalall(t), 
bind-df-next: bind-df-next(F;dfpY;s;m)
FDL editor aliases : 
bind-df-program
dfpX
>>=  dfpY  ==
    let  Abg,S,s,F  =  dfpX
    in  <B
          ,  S?  \mtimes{}  bag(a:A  \mtimes{}  (fst(snd((dfpY  a)))))
          ,  <inl  s  ,  \{\}>
          ,  \mlambda{}s,m.evalall(bind-df-next(F;dfpY;s;m))>   
Date html generated:
2011_08_16-AM-09_51_57
Last ObjectModification:
2011_06_06-PM-12_43_13
Home
Index