Nuprl Definition : hdf-compose0
hdf-compose0(f;X) == mk-hdf(X,a.let X',bs = X(a) in let out ←─ ∪b∈bs.f b in <X', out>;X.hdf-halted(X);X)
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),
callbyvalueall: callbyvalueall,
apply: f a,
spread: spread def,
pair: <a, b>,
bag-combine: ∪x∈bs.f[x]
FDL editor aliases :
hdf-compose0
hdf-compose0(f;X) == mk-hdf(X,a.let X',bs = X(a) in let out \mleftarrow{}{} \mcup{}b\mmember{}bs.f b in <X', out>X.hdf-halted(\000CX);X)
Date html generated:
2015_07_17-AM-08_05_23
Last ObjectModification:
2012_11_23-PM-02_09_28
Home
Index