Nuprl Definition : accumulate_abort
accumulate_abort(x,sofar.F[x; sofar];s;L) == eager-accum(r,x.case r of inl(sofar) => F[x; sofar] | inr(_) => r;s;L)
Definitions occuring in Statement :
eager-accum: eager-accum(x,a.f[x; a];y;l),
decide: case b of inl(x) => s[x] | inr(y) => t[y]
Definitions occuring in definition :
eager-accum: eager-accum(x,a.f[x; a];y;l),
decide: case b of inl(x) => s[x] | inr(y) => t[y]
FDL editor aliases :
accumulate_abort
Latex:
accumulate\_abort(x,sofar.F[x; sofar];s;L) ==
eager-accum(r,x.case r of inl(sofar) => F[x; sofar] | inr($_{}$) => r;s;L)
Date html generated:
2016_05_14-AM-06_55_56
Last ObjectModification:
2015_12_21-PM-05_08_53
Theory : omega
Home
Index