Nuprl Definition : hdf-bind
X >>= Y == mk-hdf(p,a.bind-nxt(Y;p;a);p.let X,ys = p 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
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:
2015_07_17-AM-08_06_51
Last ObjectModification:
2012_11_23-PM-02_10_02
Home
Index