Nuprl Definition : ler2_ChooseReply

ler2_ChooseReply(uid) ==
  let F = loc,z.
           let epoch,succ = z 
           in epoch'.if IntDeq epoch epoch' then {ler2_propose'send() succ <epoch, uid loc epoch>} else {} fi  in
      F@Loc|Loc,ler2_Nbr(), ler2_choose'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|,  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_ChooseReply
ler2\_ChooseReply(uid)  ==
    let  F  =  \mlambda{}loc,z.
                      let  epoch,succ  =  z 
                      in  \mlambda{}epoch'.if  IntDeq  epoch  epoch'
                                            then  \{ler2\_propose'send()  succ  <epoch,  uid  loc  epoch>\}
                                            else  \{\}
                                            fi    in
            F@Loc|Loc,ler2\_Nbr(),  ler2\_choose'base()|


Date html generated: 2012_02_20-PM-06_13_44
Last ObjectModification: 2012_02_02-PM-02_42_27

Home Index