Nuprl Definition : ler_ProposeReply

ler_ProposeReply(client;uid) ==
  let F = loc,zc.
           let epoch,succ = zc 
           in z.let epoch',ldr = z 
                 in if IntDeq epoch epoch'
                    then if IntDeq ldr (uid loc)
                         then {ler_send_leader() client <epoch, loc>}
                         else {ler_send_propose() succ <epoch, imax(ldr;uid loc)>}
                         fi 
                    else {}
                    fi  in
      F@Loc|Loc,Prior(ler_Nbr()), ler_Propose()|


Definitions occuring in Statement :  ler_Nbr: ler_Nbr(),  ler_send_propose: ler_send_propose(),  ler_Propose: ler_Propose(),  ler_send_leader: ler_send_leader(),  concat-lifting-loc-2: f@Loc,  simple-loc-comb-2: F|Loc,X, Y|,  primed-class: Prior(X),  imax: imax(a;b),  ifthenelse: if b then t else f fi ,  let: let,  apply: f a,  lambda: x.A[x],  spread: spread def,  pair: <a, b>,  int-deq: IntDeq,  single-bag: {x},  empty-bag: {}
FDL editor aliases :  ler_ProposeReply
ler\_ProposeReply(client;uid)  ==
    let  F  =  \mlambda{}loc,zc.
                      let  epoch,succ  =  zc 
                      in  \mlambda{}z.let  epoch',ldr  =  z 
                                  in  if  IntDeq  epoch  epoch'
                                        then  if  IntDeq  ldr  (uid  loc)
                                                  then  \{ler\_send\_leader()  client  <epoch,  loc>\}
                                                  else  \{ler\_send\_propose()  succ  <epoch,  imax(ldr;uid  loc)>\}
                                                  fi 
                                        else  \{\}
                                        fi    in
            F@Loc|Loc,Prior(ler\_Nbr()),  ler\_Propose()|


Date html generated: 2012_02_20-PM-06_00_49
Last ObjectModification: 2012_02_02-PM-02_37_44

Home Index