Nuprl Definition : base-process-class-program
base-process-class-program(X;loc;hdr) ==
λi.mk-hdf(P,m.if test-msg-header-and-loc(m;hdr;loc) then P(snd(msg-body(m))) else <P, {}> fi ;s.hdf-halted(s);X loc)
Definitions occuring in Statement :
test-msg-header-and-loc: test-msg-header-and-loc(msg;hdr;loc),
msg-body: msg-body(msg),
mk-hdf: mk-hdf(s,m.G[s; m];st.H[st];s0),
hdf-halted: hdf-halted(P),
hdf-ap: X(a),
ifthenelse: if b then t else f fi ,
pi2: snd(t),
apply: f a,
lambda: λx.A[x],
pair: <a, b>,
empty-bag: {}
FDL editor aliases :
base-process-class-program
Latex:
base-process-class-program(X;loc;hdr) ==
\mlambda{}i.mk-hdf(P,m.if test-msg-header-and-loc(m;hdr;loc)
then P(snd(msg-body(m)))
else <P, \{\}>
fi ;s.hdf-halted(s);X loc)
Date html generated:
2016_05_17-AM-09_08_13
Last ObjectModification:
2014_08_06-PM-01_48_10
Theory : local!classes
Home
Index