Nuprl Definition : ml-accum-abort

ml-accum-abort(f;sofar;L) ==
  fix((λacca,f,sofar,L. if null(L) ∨bisr(sofar) then sofar else let x.y = L in acca(f)(f(x)(outl(sofar)))(y) fi ))(f)(so\000Cfar)(L)


Definitions occuring in Statement :  spreadcons: spreadcons,  ml_apply: f(x),  null: null(as),  bor: p ∨bq,  outl: outl(x),  ifthenelse: if b then t else f fi ,  isr: isr(x),  fix: fix(F),  lambda: λx.A[x]
Definitions occuring in definition :  fix: fix(F),  lambda: λx.A[x],  ifthenelse: if b then t else f fi ,  bor: p ∨bq,  null: null(as),  isr: isr(x),  spreadcons: spreadcons,  ml_apply: f(x),  outl: outl(x)
FDL editor aliases :  ml-accum-abort
Latex:
ml-accum-abort(f;sofar;L)  ==
    fix((\mlambda{}acca,f,sofar,L.  if  null(L)  \mvee{}\msubb{}isr(sofar)
                                              then  sofar
                                              else  let  x.y  =  L 
                                                        in  acca(f)(f(x)(outl(sofar)))(y)
                                              fi  ))(f)(sofar)(L)


Date html generated: 2017_09_29-PM-05_57_09
Last ObjectModification: 2017_05_21-PM-04_37_25

Theory : omega


Home Index