Nuprl Definition : new_23_sig_headers_type
new_23_sig_headers_type{i:l}(Cmd;notify;propose) ==
{f:Name ─→ ValueAllType|
new_23_sig_headers_no_rep(notify;propose)
∧ (∀hdr∈new_23_sig_headers(notify;propose).(f hdr) = (new_23_sig_headers_fun(Cmd;notify;propose) hdr) ∈ Type)}
Definitions occuring in Statement :
new_23_sig_headers_fun: new_23_sig_headers_fun(Cmd;notify;propose),
new_23_sig_headers_no_rep: new_23_sig_headers_no_rep(notify;propose),
new_23_sig_headers: new_23_sig_headers(notify;propose),
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 :
new_23_sig_headers_type
Latex:
new\_23\_sig\_headers\_type\{i:l\}(Cmd;notify;propose) ==
\{f:Name {}\mrightarrow{} ValueAllType|
new\_23\_sig\_headers\_no\_rep(notify;propose)
\mwedge{} (\mforall{}hdr\mmember{}new\_23\_sig\_headers(notify;propose).(f hdr)
= (new\_23\_sig\_headers\_fun(Cmd;notify;propose) hdr))\}
Date html generated:
2015_07_23-PM-03_49_39
Last ObjectModification:
2013_11_23-PM-09_54_12
Home
Index