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