Nuprl Definition : taba

taba(init;x,x',a.F[x; x'; a];l) ==  fst(rec-case(l) of [] => <init, l> | x::xs' => p.let a,ys = p in let h,t = ys in <F[\000Cx; h; a], t>)


Definitions occuring in Statement :  list_ind: list_ind,  pi1: fst(t),  spread: spread def,  pair: <a, b>
Definitions occuring in definition :  pi1: fst(t),  list_ind: list_ind,  spread: spread def,  pair: <a, b>
FDL editor aliases :  taba
Latex:
taba(init;x,x',a.F[x;  x';  a];l)  ==
    fst(rec-case(l)  of
            []  =>  <init,  l>
            x::xs'  =>
              p.let  a,ys  =  p 
                  in  let  h,t  =  ys 
                        in  <F[x;  h;  a],  t>)


Date html generated: 2016_05_15-PM-07_35_31
Last ObjectModification: 2015_09_23-AM-08_17_08

Theory : general


Home Index