Nuprl Definition : simple-hdf-buffer2

simple-hdf-buffer2(X;bs) ==
  mk-hdf(Xbs,a.let X,bs Xbs 
               in let X',fs X(a) 
                  in let bs' ←─ ∪f∈fs.bag-map(f;bs)
                     in <<X', if bag-null(bs') then bs else bs' fi >bs'>;s.ff;<X, bs>)



Definitions occuring in Statement :  mk-hdf: mk-hdf(s,m.G[s; m];st.H[st];s0) hdf-ap: X(a) callbyvalueall: callbyvalueall ifthenelse: if then else fi  bfalse: ff spread: spread def pair: <a, b> bag-combine: x∈bs.f[x] bag-null: bag-null(bs) bag-map: bag-map(f;bs)
FDL editor aliases :  simple-hdf-buffer2
simple-hdf-buffer2(X;bs)  ==
    mk-hdf(Xbs,a.let  X,bs  =  Xbs 
                              in  let  X',fs  =  X(a) 
                                    in  let  bs'  \mleftarrow{}{}  \mcup{}f\mmember{}fs.bag-map(f;bs)
                                          in  <<X',  if  bag-null(bs')  then  bs  else  bs'  fi  >,  bs'>s.ff;<X,  bs>)



Date html generated: 2015_07_17-AM-08_05_45
Last ObjectModification: 2012_11_23-PM-02_09_36

Home Index