Nuprl Definition : CLK_mk_reply

CLK_mk_reply(MsgType;reply;f) ==
  λslf,z,clock. let msg_val,z = z 
                in let new_msg,recipient = reply slf msg_val 
                   in {CLK_msg'send(MsgType;f) recipient <new_msg, clock>}


Definitions occuring in Statement :  CLK_msg'send: CLK_msg'send(MsgType;f),  apply: f a,  lambda: λx.A[x],  spread: spread def,  pair: <a, b>,  single-bag: {x}
FDL editor aliases :  CLK_mk_reply
Latex:
CLK\_mk\_reply(MsgType;reply;f)  ==
    \mlambda{}slf,z,clock.  let  msg$_{val}$,z  =  z 
                                in  let  new$_{msg}$,recipient  =  reply  slf  msg$_{val\mbackslash{}f\000Cf7d$ 
                                      in  \{CLK\_msg'send(MsgType;f)  recipient  <new$_{msg}$,  clock>\}


Date html generated: 2016_05_17-PM-02_44_50
Last ObjectModification: 2013_11_23-PM-09_22_29

Theory : lamport!s!clocks


Home Index