Nuprl Definition : CLK_Clock-program

CLK_Clock-program(MsgType;f) ==  state-class1-program(λslf.0;CLK_upd_clock(MsgType);CLK_msg'base-program(MsgType;f))



Definitions occuring in Statement :  CLK_upd_clock: CLK_upd_clock(MsgType) CLK_msg'base-program: CLK_msg'base-program(MsgType;f) state-class1-program: state-class1-program(init;tr;pr) lambda: λx.A[x] natural_number: $n
FDL editor aliases :  CLK_Clock-program

Latex:
CLK\_Clock-program(MsgType;f)  ==
    state-class1-program(\mlambda{}slf.0;CLK\_upd\_clock(MsgType);CLK\_msg'base-program(MsgType;f))



Date html generated: 2016_05_17-PM-02_44_42
Last ObjectModification: 2013_11_23-PM-09_22_25

Theory : lamport!s!clocks


Home Index