Nuprl Definition : hdf-bind

X >>==  mk-hdf(p,a.bind-nxt(Y;p;a);p.let X,ys in hdf-halted(X) ∧b bag-null(ys);<X, {}>)



Definitions occuring in Statement :  bind-nxt: bind-nxt(Y;p;a) mk-hdf: mk-hdf(s,m.G[s; m];st.H[st];s0) hdf-halted: hdf-halted(P) band: p ∧b q spread: spread def pair: <a, b> bag-null: bag-null(bs) empty-bag: {}
FDL editor aliases :  hdf-bind

Latex:
X  >>=  Y  ==    mk-hdf(p,a.bind-nxt(Y;p;a);p.let  X,ys  =  p  in  hdf-halted(X)  \mwedge{}\msubb{}  bag-null(ys);<X,  \{\}>)



Date html generated: 2016_05_16-AM-10_42_47
Last ObjectModification: 2012_11_23-PM-02_10_02

Theory : halting!dataflow


Home Index