Nuprl Definition : append-tuple

append-tuple(n;m;x;y) ==
  fix((λappend-tuple,n,x. if n ≤z 0 then y
                         if (n =z 1) then if m ≤z 0 then x else <x, y> fi 
                         else let a,b = x 
                              in <a, append-tuple (n - 1) b>
                         fi )) 
  n 
  x


Definitions occuring in Statement :  le_int: i ≤z j,  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  apply: f a,  fix: fix(F),  lambda: λx.A[x],  spread: spread def,  pair: <a, b>,  subtract: n - m,  natural_number: $n
Definitions occuring in definition :  fix: fix(F),  lambda: λx.A[x],  eq_int: (i =z j),  ifthenelse: if b then t else f fi ,  le_int: i ≤z j,  spread: spread def,  pair: <a, b>,  apply: f a,  subtract: n - m,  natural_number: $n
FDL editor aliases :  append-tuple
Latex:
append-tuple(n;m;x;y)  ==
    fix((\mlambda{}append-tuple,n,x.  if  n  \mleq{}z  0  then  y
                                                  if  (n  =\msubz{}  1)  then  if  m  \mleq{}z  0  then  x  else  <x,  y>  fi 
                                                  else  let  a,b  =  x 
                                                            in  <a,  append-tuple  (n  -  1)  b>
                                                  fi  )) 
    n 
    x


Date html generated: 2016_05_14-PM-03_58_40
Last ObjectModification: 2015_09_22-PM-06_02_02

Theory : tuples


Home Index