Nuprl Definition : CLK_headers_type
CLK_headers_type{i:l}(MsgType) ==
{f:Name ─→ ValueAllType| CLK_headers_no_rep() ∧ (∀hdr∈CLK_headers().(f hdr) = (CLK_headers_fun(MsgType) hdr) ∈ Type)}
Definitions occuring in Statement :
CLK_headers_fun: CLK_headers_fun(MsgType),
CLK_headers_no_rep: CLK_headers_no_rep(),
CLK_headers: CLK_headers(),
name: Name,
l_all: (∀x∈L.P[x]),
vatype: ValueAllType,
and: P ∧ Q,
set: {x:A| B[x]} ,
apply: f a,
function: x:A ─→ B[x],
universe: Type,
equal: s = t ∈ T
FDL editor aliases :
CLK_headers_type
Latex:
CLK\_headers\_type\{i:l\}(MsgType) ==
\{f:Name {}\mrightarrow{} ValueAllType|
CLK\_headers\_no\_rep() \mwedge{} (\mforall{}hdr\mmember{}CLK\_headers().(f hdr) = (CLK\_headers\_fun(MsgType) hdr))\}
Date html generated:
2015_07_23-PM-04_09_40
Last ObjectModification:
2013_11_23-PM-09_22_10
Home
Index