Nuprl Definition : shorten-tuple

shorten-tuple(x;n) ==  fix((λshorten-tuple,x,n. if n ≤then else shorten-tuple (snd(x)) (n 1) fi )) n



Definitions occuring in Statement :  le_int: i ≤j ifthenelse: if then else fi  pi2: snd(t) apply: a fix: fix(F) lambda: λx.A[x] subtract: m natural_number: $n
Definitions occuring in definition :  fix: fix(F) lambda: λx.A[x] ifthenelse: if then else fi  le_int: i ≤j apply: a pi2: snd(t) subtract: 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