Nuprl Definition : mu_ex_v5_HandleToken
mu_ex_v5_HandleToken(initial_token;m1;m2;proc1) ==
let F = 
l,zl,z.
let interested,token,toreply = z in
if interested 
(
token)
then {mu_ex_v5_send_enter_cs() (mu_ex_v5_getMachine(m1;m2;proc1) l) 
}
else {}
fi in
F@Loc|Loc,mu_ex_v5_Token(), mu_ex_v5_PrState(initial_token)|
Definitions occuring in Statement :
mu_ex_v5_PrState: mu_ex_v5_PrState(initial_token),
mu_ex_v5_getMachine: mu_ex_v5_getMachine(m1;m2;proc1),
mu_ex_v5_send_enter_cs: mu_ex_v5_send_enter_cs(),
mu_ex_v5_Token: mu_ex_v5_Token(),
concat-lifting-loc-2: f@Loc,
simple-loc-comb-2: F|Loc,X, Y|,
band: p q,
bnot: b,
ifthenelse: if b then t else f fi ,
let: let,
it: ,
spreadn: spread3,
apply: f a,
lambda: x.A[x],
single-bag: {x},
empty-bag: {}
FDL editor aliases :
mu_ex_v5_HandleToken
mu\_ex\_v5\_HandleToken(initial$_{token}$;m1;m2;proc1) ==
let F = \mlambda{}l,zl,z.
let interested,token,toreply = z in
if interested \mwedge{}\msubb{} (\mneg{}\msubb{}token)
then \{mu\_ex\_v5\_send\_enter\_cs() (mu\_ex\_v5\_getMachine(m1;m2;proc1) l) \mcdot{}\}
else \{\}
fi in
F@Loc|Loc,mu\_ex\_v5\_Token(), mu\_ex\_v5\_PrState(initial$_{token}$)|
Date html generated:
2012_02_20-PM-06_56_02
Last ObjectModification:
2012_02_02-PM-02_59_11
Home
Index