Nuprl Definition : hdf-union

X + Y ==
  mk-hdf(XY,a.let X,Y = XY 
              in let X',xs = X(a) 
                 in let Y',ys = Y(a) 
                    in let out ←─ bag-map(λx.(inl x);xs) + bag-map(λx.(inr x );ys)
                       in <<X', Y'>, out>;XY.let X,Y = XY 
                                          in hdf-halted(X) ∧b hdf-halted(Y);<X, Y>)


Definitions occuring in Statement :  mk-hdf: mk-hdf(s,m.G[s; m];st.H[st];s0),  hdf-halted: hdf-halted(P),  hdf-ap: X(a),  band: p ∧b q,  callbyvalueall: callbyvalueall,  lambda: λx.A[x],  spread: spread def,  pair: <a, b>,  inr: inr x ,  inl: inl x,  bag-append: as + bs,  bag-map: bag-map(f;bs)
FDL editor aliases :  hdf-union
X  +  Y  ==
    mk-hdf(XY,a.let  X,Y  =  XY 
                            in  let  X',xs  =  X(a) 
                                  in  let  Y',ys  =  Y(a) 
                                        in  let  out  \mleftarrow{}{}  bag-map(\mlambda{}x.(inl  x);xs)  +  bag-map(\mlambda{}x.(inr  x  );ys)
                                              in  <<X',  Y'>,  out>XY.let  X,Y  =  XY 
                                                                                    in  hdf-halted(X)  \mwedge{}\msubb{}  hdf-halted(Y);<X,  Y>)


Date html generated: 2015_07_17-AM-08_06_29
Last ObjectModification: 2012_11_23-PM-02_09_57

Home Index