Nuprl Definition : hdf-state1-single-val
hdf-state1-single-val(f;X;b) ==
mk-hdf(Xb,a.let X,b = Xb
in let X',xs = X(a)
in let b' ←─ if bag-null(xs) then b else f sv-bag-only(xs) b fi
in <<X', b'>, {b'}>;s.ff;<X, b>)
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
,
apply: f a
,
spread: spread def,
pair: <a, b>
,
sv-bag-only: sv-bag-only(b)
,
bag-null: bag-null(bs)
,
single-bag: {x}
FDL editor aliases :
hdf-state1-single-val
hdf-state1-single-val(f;X;b) ==
mk-hdf(Xb,a.let X,b = Xb
in let X',xs = X(a)
in let b' \mleftarrow{}{} if bag-null(xs) then b else f sv-bag-only(xs) b fi
in <<X', b'>, \{b'\}>s.ff;<X, b>)
Date html generated:
2015_07_17-AM-08_05_56
Last ObjectModification:
2012_11_23-PM-02_09_44
Home
Index