Nuprl Definition : ap2-tuple

ap2-tuple(len;f;x;t) ==
  fix((λap2-tuple,len,f,t. if (len =z 0) then t
                          if (len =z 1) then f x t
                          else <(fst(f)) x (fst(t)), ap2-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 :  ap2-tuple
Latex:
ap2-tuple(len;f;x;t)  ==
    fix((\mlambda{}ap2-tuple,len,f,t.  if  (len  =\msubz{}  0)  then  t
                                                    if  (len  =\msubz{}  1)  then  f  x  t
                                                    else  <(fst(f))  x  (fst(t)),  ap2-tuple  (len  -  1)  (snd(f))  (snd(t))>
                                                    fi  )) 
    len 
    f 
    t


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

Theory : tuples


Home Index