bind-df-program1(A;B;dfpX;dfpY) ==
let Abg,S,s,F = dfpX
in <B
, S? 
bag(a:A (fst(snd((dfpY a)))?))
, <inl s , {}>
, 
s,m.bind-df-next1(F;dfpY;s;m)>
Definitions occuring in Statement :
bind-df-next1: bind-df-next1(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)
Definitions :
spreadn: spread4,
bag: bag(T),
product: x:A B[x],
union: left + right,
pi1: fst(t),
pi2: snd(t),
apply: f a,
unit: Unit,
pair: <a, b>,
inl: inl x ,
empty-bag: {},
lambda: x.A[x],
bind-df-next1: bind-df-next1(F;dfpY;s;m)
FDL editor aliases :
bind-df-program1
bind-df-program1(A;B;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.bind-df-next1(F;dfpY;s;m)>
Date html generated:
2011_08_16-AM-09_51_11
Last ObjectModification:
2011_05_07-PM-02_33_53
Home
Index