Nuprl Definition : hdf-rec-bind

hdf-rec-bind(X;Y) ==  λv.mk-hdf(p,a.rec-bind-nxt(X;Y;p;a);p.let xs,ys = p in bag-null(xs) ∧b bag-null(ys);<{X v}, {Y v}>\000C)


Definitions occuring in Statement :  rec-bind-nxt: rec-bind-nxt(X;Y;p;a),  mk-hdf: mk-hdf(s,m.G[s; m];st.H[st];s0),  band: p ∧b q,  apply: f a,  lambda: λx.A[x],  spread: spread def,  pair: <a, b>,  bag-null: bag-null(bs),  single-bag: {x}
FDL editor aliases :  hdf-rec-bind
hdf-rec-bind(X;Y)  ==
    \mlambda{}v.mk-hdf(p,a.rec-bind-nxt(X;Y;p;a);p.let  xs,ys  =  p 
                                                                                in  bag-null(xs)  \mwedge{}\msubb{}  bag-null(ys);<\{X  v\},  \{Y  v\}>)


Date html generated: 2015_07_17-AM-08_08_02
Last ObjectModification: 2012_11_23-PM-02_10_10

Home Index