Nuprl Definition : recode-tuple

recode-tuple(f) ==
  λL.rec-case(L) of
     [] => <[], λx.x, λx.x>
     T::Ts =>
      r.let l2,h2,j2 = r in 
     let l1,h1,j1 = f T in 
     if null(Ts)
     then <l1, h1, j1>
     else <l1 @ l2
          , λx.let a,b = x 
               in append-tuple(||l1||;||l2||;h1 a;h2 b)
          , if null(l2) then λx.<j1 x, j2 ⋅> else λx.let a,b = split-tuple(x;||l1||) in <j1 a, j2 b> fi >
     fi 


Definitions occuring in Statement :  append-tuple: append-tuple(n;m;x;y),  split-tuple: split-tuple(x;n),  length: ||as||,  null: null(as),  append: as @ bs,  list_ind: list_ind,  nil: [],  ifthenelse: if b then t else f fi ,  it: ⋅,  spreadn: spread3,  apply: f a,  lambda: λx.A[x],  spread: spread def,  pair: <a, b>
Definitions occuring in definition :  list_ind: list_ind,  nil: [],  spreadn: spread3,  append: as @ bs,  append-tuple: append-tuple(n;m;x;y),  ifthenelse: if b then t else f fi ,  null: null(as),  it: ⋅,  lambda: λx.A[x],  spread: spread def,  split-tuple: split-tuple(x;n),  length: ||as||,  pair: <a, b>,  apply: f a
FDL editor aliases :  recode-tuple
Latex:
recode-tuple(f)  ==
    \mlambda{}L.rec-case(L)  of
          []  =>  <[],  \mlambda{}x.x,  \mlambda{}x.x>
          T::Ts  =>
            r.let  l2,h2,j2  =  r  in 
          let  l1,h1,j1  =  f  T  in 
          if  null(Ts)
          then  <l1,  h1,  j1>
          else  <l1  @  l2
                    ,  \mlambda{}x.let  a,b  =  x 
                              in  append-tuple(||l1||;||l2||;h1  a;h2  b)
                    ,  if  null(l2)
                    then  \mlambda{}x.<j1  x,  j2  \mcdot{}>
                    else  \mlambda{}x.let  a,b  =  split-tuple(x;||l1||) 
                                    in  <j1  a,  j2  b>
                    fi  >
          fi 


Date html generated: 2016_05_15-PM-05_49_09
Last ObjectModification: 2015_09_23-AM-07_59_18

Theory : general


Home Index