Nuprl Definition : pRun
pRun(S0;env;nat2msg;loc2msg) ==
Y
(λpRun,t. if (t =z 0)
then <inr ⋅ , S0>
else let n,m,nm = env t pRun in
do-chosen-command(nat2msg;loc2msg;t;snd((pRun (t - 1)));n;m;nm)
fi )
Definitions occuring in Statement :
do-chosen-command: do-chosen-command(nat2msg;loc2msg;t;S;n;m;nm)
,
ifthenelse: if b then t else f fi
,
eq_int: (i =z j)
,
it: ⋅
,
spreadn: spread3,
pi2: snd(t)
,
ycomb: Y
,
apply: f a
,
lambda: λx.A[x]
,
pair: <a, b>
,
inr: inr x
,
subtract: n - m
,
natural_number: $n
FDL editor aliases :
pRun
Latex:
pRun(S0;env;nat2msg;loc2msg) ==
Y
(\mlambda{}pRun,t. if (t =\msubz{} 0)
then <inr \mcdot{} , S0>
else let n,m,nm = env t pRun in
do-chosen-command(nat2msg;loc2msg;t;snd((pRun (t - 1)));n;m;nm)
fi )
Date html generated:
2015_07_23-AM-11_09_41
Last ObjectModification:
2012_02_25-PM-03_40_17
Home
Index