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