Nuprl Definition : collect_accum

collect_accum(x.num[x];init;a,v.f[a; v];a.P[a]) ==
  λs,v. eval num[v] in
        let i,a,w in 
        if n <then <i, a, inr 0 >
        if i <then if P[f[init; v]] then <1, init, inl f[init; v]> else <n, f[init; v], inr 0 > fi 
        if P[f[a; v]] then <1, init, inl f[a; v]>
        else <i, f[a; v], inr 0 >
        fi 



Definitions occuring in Statement :  callbyvalue: callbyvalue ifthenelse: if then else fi  lt_int: i <j spreadn: spread3 lambda: λx.A[x] pair: <a, b> inr: inr  inl: inl x add: m natural_number: $n
FDL editor aliases :  collect_accum collect_accum

Latex:
collect\_accum(x.num[x];init;a,v.f[a;  v];a.P[a])  ==
    \mlambda{}s,v.  eval  n  =  num[v]  in
                let  i,a,w  =  s  in 
                if  n  <z  i  then  <i,  a,  inr  0  >
                if  i  <z  n
                    then  if  P[f[init;  v]]  then  <n  +  1,  init,  inl  f[init;  v]>  else  <n,  f[init;  v],  inr  0  >  fi 
                if  P[f[a;  v]]  then  <i  +  1,  init,  inl  f[a;  v]>
                else  <i,  f[a;  v],  inr  0  >
                fi 



Date html generated: 2016_05_16-AM-10_11_32
Last ObjectModification: 2013_03_25-PM-01_55_02

Theory : new!event-ordering


Home Index