Nuprl Definition : shorten-tuple
shorten-tuple(x;n) == fix((λshorten-tuple,x,n. if n ≤z 0 then x else shorten-tuple (snd(x)) (n - 1) fi )) x n
Definitions occuring in Statement :
le_int: i ≤z j,
ifthenelse: if b then t else f fi ,
pi2: snd(t),
apply: f a,
fix: fix(F),
lambda: λx.A[x],
subtract: n - m,
natural_number: $n
Definitions occuring in definition :
fix: fix(F),
lambda: λx.A[x],
ifthenelse: if b then t else f fi ,
le_int: i ≤z j,
apply: f a,
pi2: snd(t),
subtract: n - m,
natural_number: $n
FDL editor aliases :
shorten-tuple
Latex:
shorten-tuple(x;n) ==
fix((\mlambda{}shorten-tuple,x,n. if n \mleq{}z 0 then x else shorten-tuple (snd(x)) (n - 1) fi )) x n
Date html generated:
2016_05_14-PM-03_58_33
Last ObjectModification:
2015_09_22-PM-06_02_01
Theory : tuples
Home
Index