Nuprl Definition : CLK_headers_fun
CLK_headers_fun(MsgType) == λhdr.if name_eq(hdr;``CLK msg``) then MsgType × ℤ else Top fi
Definitions occuring in Statement :
name_eq: name_eq(x;y),
cons: [a / b],
nil: [],
ifthenelse: if b then t else f fi ,
top: Top,
lambda: λx.A[x],
product: x:A × B[x],
int: ℤ,
token: "$token"
FDL editor aliases :
CLK_headers_fun
Latex:
CLK\_headers\_fun(MsgType) == \mlambda{}hdr.if name\_eq(hdr;``CLK msg``) then MsgType \mtimes{} \mBbbZ{} else Top fi
Date html generated:
2015_07_23-PM-04_09_38
Last ObjectModification:
2013_11_23-PM-09_22_08
Home
Index