Nuprl Definition : header-type-spec
header-type-spec{i:l}(L;g) == {f:Name ─→ ValueAllType| no_repeats(Name;L) ∧ (∀hdr∈L.(f hdr) = (g hdr) ∈ Type)}
Definitions occuring in Statement :
name: Name,
l_all: (∀x∈L.P[x]),
no_repeats: no_repeats(T;l),
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 :
header-type-spec
Latex:
header-type-spec\{i:l\}(L;g) ==
\{f:Name {}\mrightarrow{} ValueAllType| no\_repeats(Name;L) \mwedge{} (\mforall{}hdr\mmember{}L.(f hdr) = (g hdr))\}
Date html generated:
2015_07_21-PM-04_48_04
Last ObjectModification:
2013_04_25-PM-02_01_21
Home
Index