Nuprl Definition : hdf-state

hdf-state(X;bs) ==
  mk-hdf(Xbs,a.let X,s = Xbs 
               in let X',fs = X(a) 
                  in let b ←─ ∪f∈fs.bag-map(f;s)
                     in let s' ←─ if bag-null(b) then s else b fi 
                        in <<X', s'>, s'>;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 b then t else f 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 :  hdf-state
hdf-state(X;bs)  ==
    mk-hdf(Xbs,a.let  X,s  =  Xbs 
                              in  let  X',fs  =  X(a) 
                                    in  let  b  \mleftarrow{}{}  \mcup{}f\mmember{}fs.bag-map(f;s)
                                          in  let  s'  \mleftarrow{}{}  if  bag-null(b)  then  s  else  b  fi 
                                                in  <<X',  s'>,  s'>s.ff;<X,  bs>)


Date html generated: 2015_07_17-AM-08_05_48
Last ObjectModification: 2012_11_23-PM-02_09_38

Home Index