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