Nuprl Definition : collect_accm

collect_accm(v.P[v];v.num[v]) ==
  λ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 


Definitions occuring in Statement :  append: as @ bs,  cons: [a / b],  nil: [],  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_accm collect_accm
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: 2015_07_17-AM-08_59_40
Last ObjectModification: 2013_03_25-PM-01_54_58

Home Index