Nuprl Definition : CLK_Clock
CLK_Clock(MsgType;f) == state-class1(λslf.0;CLK_upd_clock(MsgType);CLK_msg'base(MsgType;f))
Definitions occuring in Statement :
CLK_upd_clock: CLK_upd_clock(MsgType),
CLK_msg'base: CLK_msg'base(MsgType;f),
state-class1: state-class1(init;tr;X),
lambda: λx.A[x],
natural_number: $n
FDL editor aliases :
CLK_Clock
Latex:
CLK\_Clock(MsgType;f) == state-class1(\mlambda{}slf.0;CLK\_upd\_clock(MsgType);CLK\_msg'base(MsgType;f))
Date html generated:
2015_07_23-PM-04_09_48
Last ObjectModification:
2013_11_23-PM-09_22_18
Home
Index