Nuprl Definition : map-tuple

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


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

Theory : tuples


Home Index