Nuprl Definition : ler2_ProposeReply

ler2_ProposeReply(client;uid) ==
  let F = loc,zb.
           let epoch,succ = zb 
           in z.let epoch',ldr = z 
                 in if IntDeq epoch epoch'
                    then if IntDeq ldr (uid loc epoch)
                         then {ler2_leader'send() client <epoch, loc>}
                         else {ler2_propose'send() succ <epoch, imax(ldr;uid loc epoch)>}
                         fi 
                    else {}
                    fi  in
      F@Loc|Loc,ler2_Nbr(), ler2_propose'base()|


Definitions occuring in Statement :  ler2_Nbr: ler2_Nbr(),  ler2_propose'send: ler2_propose'send(),  concat-lifting-loc-2: f@Loc,  simple-loc-comb-2: F|Loc,X, Y|,  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 :  ler2_ProposeReply
ler2\_ProposeReply(client;uid)  ==
    let  F  =  \mlambda{}loc,zb.
                      let  epoch,succ  =  zb 
                      in  \mlambda{}z.let  epoch',ldr  =  z 
                                  in  if  IntDeq  epoch  epoch'
                                        then  if  IntDeq  ldr  (uid  loc  epoch)
                                                  then  \{ler2\_leader'send()  client  <epoch,  loc>\}
                                                  else  \{ler2\_propose'send()  succ  <epoch,  imax(ldr;uid  loc  epoch)>\}
                                                  fi 
                                        else  \{\}
                                        fi    in
            F@Loc|Loc,ler2\_Nbr(),  ler2\_propose'base()|


Date html generated: 2012_02_20-PM-06_13_27
Last ObjectModification: 2012_02_02-PM-02_42_14

Home Index