Nuprl Definition : hdf-compose0

hdf-compose0(f;X) ==  mk-hdf(X,a.let X',bs X(a) in let out ←─ ∪b∈bs.f 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: 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