Nuprl Definition : tuple
tuple(n;i.F[i]) == rec-case(map(λi.F[i];upto(n))) of [] => ⋅ | a::as => r.if null(as) then a else <a, r> fi
Definitions occuring in Statement :
upto: upto(n),
null: null(as),
map: map(f;as),
list_ind: list_ind,
ifthenelse: if b then t else f fi ,
it: ⋅,
lambda: λx.A[x],
pair: <a, b>
Definitions occuring in definition :
list_ind: list_ind,
map: map(f;as),
lambda: λx.A[x],
upto: upto(n),
it: ⋅,
ifthenelse: if b then t else f fi ,
null: null(as),
pair: <a, b>
FDL editor aliases :
tuple
Latex:
tuple(n;i.F[i]) ==
rec-case(map(\mlambda{}i.F[i];upto(n))) of
[] => \mcdot{}
a::as =>
r.if null(as) then a else <a, r> fi
Date html generated:
2016_05_14-PM-03_57_35
Last ObjectModification:
2015_09_22-PM-06_01_58
Theory : tuples
Home
Index