Nuprl Definition : convolution

convolution(a,b,c.f[a; b; c];c0;L1;L2) ==
  cps-accum(k,a.λp.let remaining,c = p in rec-case(remaining) of [] => k p | b::bs => r.k <bs, f[a; b; c]>;<L2, c0>;L1) \000C(λp.(snd(p)))


Definitions occuring in Statement :  cps-accum: cps-accum(k,a.f[k; a];b;L),  list_ind: list_ind,  pi2: snd(t),  apply: f a,  lambda: λx.A[x],  spread: spread def,  pair: <a, b>
Definitions occuring in definition :  cps-accum: cps-accum(k,a.f[k; a];b;L),  spread: spread def,  list_ind: list_ind,  apply: f a,  pair: <a, b>,  lambda: λx.A[x],  pi2: snd(t)
FDL editor aliases :  convolution
Latex:
convolution(a,b,c.f[a;  b;  c];c0;L1;L2)  ==
    cps-accum(k,a.\mlambda{}p.let  remaining,c  =  p 
                                      in  rec-case(remaining)  of
                                            []  =>  k  p
                                            b::bs  =>
                                              r.k  <bs,  f[a;  b;  c]><L2,  c0>L1) 
    (\mlambda{}p.(snd(p)))


Date html generated: 2016_05_15-PM-03_48_32
Last ObjectModification: 2015_09_23-AM-07_44_57

Theory : general


Home Index