Nuprl Definition : bind-nextouts1

bind-nextouts1(L;dfpY;m) ==
  bag-map(p.let a,s = p 
             in case s
                of inl(s) =>
                 let s',out = df-program-in-state-ap(dfpY a;s;m) 
                 in <<a, s'>, out>
                 | inr(z) =>
                 <<a, s>, {}>;L)


Definitions occuring in Statement :  df-program-in-state-ap: df-program-in-state-ap(dfp;s;m),  apply: f a,  lambda: x.A[x],  spread: spread def,  pair: <a, b>,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  bag-map: bag-map(f;bs),  empty-bag: {}
FDL editor aliases :  bind-nextouts1
bind-nextouts1(L;dfpY;m)  ==
    bag-map(\mlambda{}p.let  a,s  =  p 
                          in  case  s
                                of  inl(s)  =>
                                  let  s',out  =  df-program-in-state-ap(dfpY  a;s;m) 
                                  in  <<a,  s'>,  out>
                                  |  inr(z)  =>
                                  <<a,  s>,  \{\}>L)


Date html generated: 2012_01_23-PM-12_01_09
Last ObjectModification: 2011_12_16-PM-06_11_30

Home Index