Nuprl Definition : pv11_p1_when_adopted

pv11_p1_when_adopted(Cmd;ldrs_uid) ==
  λloc,zr,z. let bnum,pvals = zr 
             in let ballot_num,active,proposals = z in 
                if pv11_p1_eq_bnums() bnum ballot_num
                then let proposals' = pv11_p1_update_proposals(Cmd) proposals (pv11_p1_pmax(Cmd;ldrs_uid) pvals) in
                         <ballot_num, tt, proposals'>
                else <ballot_num, active, proposals>
                fi 


Definitions occuring in Statement :  pv11_p1_update_proposals: pv11_p1_update_proposals(Cmd),  pv11_p1_pmax: pv11_p1_pmax(Cmd;ldrs_uid),  pv11_p1_eq_bnums: pv11_p1_eq_bnums(),  ifthenelse: if b then t else f fi ,  btrue: tt,  let: let,  spreadn: spread3,  apply: f a,  lambda: λx.A[x],  spread: spread def,  pair: <a, b>
FDL editor aliases :  pv11_p1_when_adopted
Latex:
pv11\_p1\_when\_adopted(Cmd;ldrs$_{uid}$)  ==
    \mlambda{}loc,zr,z.  let  bnum,pvals  =  zr 
                          in  let  ballot$_{num}$,active,proposals  =  z  in 
                                if  pv11\_p1\_eq\_bnums()  bnum  ballot$_{num}$
                                then  let  proposals'  =  pv11\_p1\_update\_proposals(Cmd)  proposals 
                                                                            (pv11\_p1\_pmax(Cmd;ldrs$_{uid}$)  pvals)  in
                                                  <ballot$_{num}$,  tt,  proposals'>
                                else  <ballot$_{num}$,  active,  proposals>
                                fi 


Date html generated: 2015_07_23-PM-04_32_57
Last ObjectModification: 2014_11_26-AM-11_29_29

Home Index