Nuprl Definition : update-oarcast-deliver

update-oarcast-deliver(eq;s;p) ==
  let remaining,counts = s 
  in let orderer,xxx = p 
     in if bag-deq-member(IdDeq;orderer;remaining)
        then eval rem' = eval_bag(remaining - orderer) in
             eval counts' = eval_list(weak-update-alist(eq;counts;xxx;1;n.n + 1)) in
               <rem', counts'>
        else s
        fi 


Definitions occuring in Statement :  id-deq: IdDeq,  weak-update-alist: weak-update-alist(eq;L;x;z;v.f[v]),  eval_list: eval_list(t),  callbyvalue: callbyvalue,  ifthenelse: if b then t else f fi ,  spread: spread def,  pair: <a, b>,  add: n + m,  natural_number: $n,  bag-remove: bs - x,  bag-deq-member: bag-deq-member(eq;x;b),  eval_bag: eval_bag(b)
FDL editor aliases :  update-oarcast-deliver
Latex:
update-oarcast-deliver(eq;s;p)  ==
    let  remaining,counts  =  s 
    in  let  orderer,xxx  =  p 
          in  if  bag-deq-member(IdDeq;orderer;remaining)
                then  eval  rem'  =  eval\_bag(remaining  -  orderer)  in
                          eval  counts'  =  eval\_list(weak-update-alist(eq;counts;xxx;1;n.n  +  1))  in
                              <rem',  counts'>
                else  s
                fi 


Date html generated: 2015_07_23-PM-00_28_17
Last ObjectModification: 2014_08_06-AM-11_09_58

Home Index