Nuprl Definition : cbv_list_accum

cbv_list_accum(x,a.f[x; a];y;L) ==
  fix((λcbv_list_accum,y,L. eval v = L in
                            if v is a pair then let h,t = v 
                                                in eval y' = f[y; h] in
                                                   cbv_list_accum y' t otherwise if v = Ax then y otherwise ⊥)) 
  y 
  L


Definitions occuring in Statement :  bottom: ⊥,  callbyvalue: callbyvalue,  ispair: if z is a pair then a otherwise b,  isaxiom: if z = Ax then a otherwise b,  apply: f a,  fix: fix(F),  lambda: λx.A[x],  spread: spread def
Definitions occuring in definition :  fix: fix(F),  lambda: λx.A[x],  ispair: if z is a pair then a otherwise b,  spread: spread def,  callbyvalue: callbyvalue,  apply: f a,  isaxiom: if z = Ax then a otherwise b,  bottom: ⊥
FDL editor aliases :  cbv_list_accum
Latex:
cbv\_list\_accum(x,a.f[x;  a];y;L)  ==
    fix((\mlambda{}cbv\_list$_{accum}$,y,L.  eval  v  =  L  in
                                                      if  v  is  a  pair  then  let  h,t  =  v 
                                                                                              in  eval  y'  =  f[y;  h]  in
                                                                                                    cbv\_list$_{accum}$  y'  t
                                                      otherwise  if  v  =  Ax  then  y  otherwise  \mbot{})) 
    y 
    L


Date html generated: 2017_09_29-PM-05_53_42
Last ObjectModification: 2017_05_04-PM-03_32_35

Theory : omega


Home Index