Nuprl Definition : hdf-bind-gen
X (hdfs) >>= Y == mk-hdf(p,a.bind-nxt(Y;p;a);p.let X,ys = p in hdf-halted(X) ∧b bag-null(ys);<X, hdfs>)
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)
FDL editor aliases :
hdf-bind-gen
X (hdfs) >>= 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, hdfs>)
Date html generated:
2015_07_17-AM-08_06_54
Last ObjectModification:
2012_11_23-PM-02_10_03
Home
Index