Nuprl Definition : collect_accm

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



Definitions occuring in Statement :  append: as bs cons: [a b] nil: [] 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_accm collect_accm

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



Date html generated: 2016_05_16-AM-10_11_03
Last ObjectModification: 2013_03_25-PM-01_54_58

Theory : new!event-ordering


Home Index