Nuprl Definition : ptuple
ptuple(lbl,p.a[lbl; p];X) ==
λparam.(labl:{lbl:Atom| 0 < ||a[lbl; param]||} × tuple-type(map(λx.case x
of inl(y) =>
case y of inl(p) => X p | inr(p) => (X p) List
| inr(E) =>
E;a[labl; param])))
Definitions occuring in Statement :
tuple-type: tuple-type(L),
length: ||as||,
map: map(f;as),
list: T List,
less_than: a < b,
set: {x:A| B[x]} ,
apply: f a,
lambda: λx.A[x],
product: x:A × B[x],
decide: case b of inl(x) => s[x] | inr(y) => t[y],
natural_number: $n,
atom: Atom
Definitions occuring in definition :
product: x:A × B[x],
set: {x:A| B[x]} ,
atom: Atom,
less_than: a < b,
natural_number: $n,
length: ||as||,
tuple-type: tuple-type(L),
map: map(f;as),
lambda: λx.A[x],
decide: case b of inl(x) => s[x] | inr(y) => t[y],
list: T List,
apply: f a
FDL editor aliases :
ptuple
Latex:
ptuple(lbl,p.a[lbl; p];X) ==
\mlambda{}param.(labl:\{lbl:Atom| 0 < ||a[lbl; param]||\} \mtimes{} tuple-type(map(\mlambda{}x.case x
of inl(y) =>
case y
of inl(p) =>
X p
| inr(p) =>
(X p) List
| inr(E) =>
E;a[labl; param])))
Date html generated:
2019_06_20-PM-02_03_49
Last ObjectModification:
2019_02_22-PM-03_13_13
Theory : tuples
Home
Index