Nuprl Definition : collect_accum

collect_accum(x.num[x];init;a,v.f[a; v];a.P[a]) ==
  λ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 


Definitions occuring in Statement :  callbyvalue: callbyvalue,  ifthenelse: if b then t else f fi ,  lt_int: i <z j,  spreadn: spread3,  lambda: λx.A[x],  pair: <a, b>,  inr: inr x ,  inl: inl x,  add: n + m,  natural_number: $n
FDL editor aliases :  collect_accum collect_accum
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: 2015_07_17-AM-08_59_50
Last ObjectModification: 2013_03_25-PM-01_55_02

Home Index