Nuprl Definition : hdf-once
hdf-once(X) == mk-hdf(X,a.let X',b = X(a) in <if bag-null(b) then X' else hdf-halt() fi , b>;X.hdf-halted(X);X)
Definitions occuring in Statement :
mk-hdf: mk-hdf(s,m.G[s; m];st.H[st];s0),
hdf-halt: hdf-halt(),
hdf-halted: hdf-halted(P),
hdf-ap: X(a),
ifthenelse: if b then t else f fi ,
spread: spread def,
pair: <a, b>,
bag-null: bag-null(bs)
FDL editor aliases :
hdf-once
hdf-once(X) ==
mk-hdf(X,a.let X',b = X(a)
in <if bag-null(b) then X' else hdf-halt() fi , b>X.hdf-halted(X);X)
Date html generated:
2015_07_17-AM-08_06_04
Last ObjectModification:
2012_11_23-PM-02_09_50
Home
Index