Nuprl Definition : CLK_headers_no_inputs_types
CLK_headers_no_inputs_types(MsgType) ==  [<``CLK msg``, MsgType × ℤ>]
Definitions occuring in Statement : 
cons: [a / b]
, 
nil: []
, 
pair: <a, b>
, 
product: x:A × B[x]
, 
int: ℤ
, 
token: "$token"
FDL editor aliases : 
CLK_headers_no_inputs_types
Latex:
CLK\_headers\_no\_inputs\_types(MsgType)  ==    [<``CLK  msg``,  MsgType  \mtimes{}  \mBbbZ{}>]
Date html generated:
2016_05_17-PM-02_45_24
Last ObjectModification:
2013_11_23-PM-09_22_44
Theory : lamport!s!clocks
Home
Index