Nuprl Definition : hdf-memory
hdf-memory(X;bs) ==
mk-hdf(Xbs,a.let X,s = Xbs
in let X',fs = X(a)
in let b ←─ ∪f∈fs.bag-map(f;s)
in let s' ←─ if bag-null(b) then s else b fi
in <<X', s'>, s>;s.ff;<X, bs>)
Definitions occuring in Statement :
mk-hdf: mk-hdf(s,m.G[s; m];st.H[st];s0),
hdf-ap: X(a),
callbyvalueall: callbyvalueall,
ifthenelse: if b then t else f fi ,
bfalse: ff,
spread: spread def,
pair: <a, b>,
bag-combine: ∪x∈bs.f[x],
bag-null: bag-null(bs),
bag-map: bag-map(f;bs)
FDL editor aliases :
hdf-memory
hdf-memory(X;bs) ==
mk-hdf(Xbs,a.let X,s = Xbs
in let X',fs = X(a)
in let b \mleftarrow{}{} \mcup{}f\mmember{}fs.bag-map(f;s)
in let s' \mleftarrow{}{} if bag-null(b) then s else b fi
in <<X', s'>, s>s.ff;<X, bs>)
Date html generated:
2015_07_17-AM-08_05_58
Last ObjectModification:
2012_11_23-PM-02_09_46
Home
Index