Nuprl Definition : pv11_p1_headers_type
pv11_p1_headers_type{i:l}(Cmd) ==
{mf:Name ─→ ValueAllType|
pv11_p1_headers_no_rep() ∧ (∀hdr∈pv11_p1_headers().(mf hdr) = (pv11_p1_headers_fun(Cmd) hdr) ∈ Type)}
Definitions occuring in Statement :
pv11_p1_headers_fun: pv11_p1_headers_fun(Cmd),
pv11_p1_headers_no_rep: pv11_p1_headers_no_rep(),
pv11_p1_headers: pv11_p1_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 :
pv11_p1_headers_type
Latex:
pv11\_p1\_headers\_type\{i:l\}(Cmd) ==
\{mf:Name {}\mrightarrow{} ValueAllType|
pv11\_p1\_headers\_no\_rep() \mwedge{} (\mforall{}hdr\mmember{}pv11\_p1\_headers().(mf hdr) = (pv11\_p1\_headers\_fun(Cmd) hdr))\}
Date html generated:
2015_07_23-PM-04_11_11
Last ObjectModification:
2014_11_26-AM-11_22_33
Home
Index