Nuprl Definition : ler_ChooseReply

ler_ChooseReply(uid) ==
  let F = loc,z.
           let epoch,succ = z 
           in epoch'.if IntDeq epoch epoch' then {ler_send_propose() succ <epoch, uid loc>} else {} fi  in
      F@Loc|Loc,Prior(ler_Nbr()), ler_Choose()|


Definitions occuring in Statement :  ler_Nbr: ler_Nbr(),  ler_send_propose: ler_send_propose(),  ler_Choose: ler_Choose(),  concat-lifting-loc-2: f@Loc,  simple-loc-comb-2: F|Loc,X, Y|,  primed-class: Prior(X),  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_ChooseReply
ler\_ChooseReply(uid)  ==
    let  F  =  \mlambda{}loc,z.
                      let  epoch,succ  =  z 
                      in  \mlambda{}epoch'.if  IntDeq  epoch  epoch'
                                            then  \{ler\_send\_propose()  succ  <epoch,  uid  loc>\}
                                            else  \{\}
                                            fi    in
            F@Loc|Loc,Prior(ler\_Nbr()),  ler\_Choose()|


Date html generated: 2012_02_20-PM-06_01_09
Last ObjectModification: 2012_02_02-PM-02_37_52

Home Index