Nuprl Definition : split-tuple

split-tuple(x;n) ==
  fix((λsplit-tuple,x,n. if (n =z 0) then <⋅, x>
                        if (n =z 1) then <fst(x), snd(x)>
                        else let a,b = split-tuple (snd(x)) (n - 1) 
                             in <<fst(x), a>, b>
                        fi )) 
  x 
  n


Definitions occuring in Statement :  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  it: ⋅,  pi1: fst(t),  pi2: snd(t),  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],  it: ⋅,  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  spread: spread def,  apply: f a,  pi2: snd(t),  subtract: n - m,  natural_number: $n,  pair: <a, b>,  pi1: fst(t)
FDL editor aliases :  split-tuple
Latex:
split-tuple(x;n)  ==
    fix((\mlambda{}split-tuple,x,n.  if  (n  =\msubz{}  0)  then  <\mcdot{},  x>
                                                if  (n  =\msubz{}  1)  then  <fst(x),  snd(x)>
                                                else  let  a,b  =  split-tuple  (snd(x))  (n  -  1) 
                                                          in  <<fst(x),  a>,  b>
                                                fi  )) 
    x 
    n


Date html generated: 2016_05_14-PM-03_58_26
Last ObjectModification: 2015_09_22-PM-06_02_01

Theory : tuples


Home Index