Nuprl Definition : select-tuple

x.n ==
  fix((λselect-tuple,len,x,n. if (n =z 0)
                             then if (len =z 1) then x else fst(x) fi 
                             else select-tuple (len - 1) (snd(x)) (n - 1)
                             fi )) 
  len 
  x 
  n


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


Date html generated: 2016_05_14-PM-03_58_08
Last ObjectModification: 2015_09_22-PM-06_02_00

Theory : tuples


Home Index