Nuprl Definition : mk-hdf
mk-hdf(s,m.G[s; m];st.H[st];s0) ==
fix((λmk-hdf,s0. if H[s0] then hdf-halt() else hdf-run(λm.let s1,b = G[s0; m] in <mk-hdf s1, b>) fi )) s0
Definitions occuring in Statement :
hdf-run: hdf-run(P),
hdf-halt: hdf-halt(),
ifthenelse: if b then t else f fi ,
apply: f a,
fix: fix(F),
lambda: λx.A[x],
spread: spread def,
pair: <a, b>
FDL editor aliases :
mk-hdf
mk-hdf(s,m.G[s; m];st.H[st];s0) ==
fix((\mlambda{}mk-hdf,s0. if H[s0]
then hdf-halt()
else hdf-run(\mlambda{}m.let s1,b = G[s0; m]
in <mk-hdf s1, b>)
fi ))
s0
Date html generated:
2015_07_17-AM-08_05_13
Last ObjectModification:
2012_11_23-PM-02_09_23
Home
Index