Nuprl Definition : ap-tuple

ap-tuple(len;f;t) ==
  fix((λap-tuple,len,f,t. if (len =z 0) then t
                         if (len =z 1) then f t
                         else <(fst(f)) (fst(t)), ap-tuple (len - 1) (snd(f)) (snd(t))>
                         fi )) 
  len 
  f 
  t


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],  pair: <a, b>,  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),  pair: <a, b>,  pi1: fst(t),  apply: f a,  subtract: n - m,  natural_number: $n,  pi2: snd(t)
FDL editor aliases :  ap-tuple
Latex:
ap-tuple(len;f;t)  ==
    fix((\mlambda{}ap-tuple,len,f,t.  if  (len  =\msubz{}  0)  then  t
                                                  if  (len  =\msubz{}  1)  then  f  t
                                                  else  <(fst(f))  (fst(t)),  ap-tuple  (len  -  1)  (snd(f))  (snd(t))>
                                                  fi  )) 
    len 
    f 
    t


Date html generated: 2016_05_14-PM-03_57_49
Last ObjectModification: 2015_09_22-PM-06_01_59

Theory : tuples


Home Index