Nuprl Definition : collect

Nuprl Definition : collect_accum

collect_accum(x.num[x];init;a,v.f[a; v];a.P[a]) ==
  λs,v. eval n = num[v] in
        let i,a,w = s in
        if n <z i then <i, a, inr 0 >

        if i <z n then if P[f[init; v]] then <n + 1, init, inl f[init; v]> else <n, f[init; v], inr 0 > fi

        if P[f[a; v]] then <i + 1, init, inl f[a; v]>
        else <i, f[a; v], inr 0 >
        fi

Definitions occuring in Statement : callbyvalue: callbyvalue, ifthenelse: if b then t else f fi , lt_int: i <z j, spreadn: spread3, lambda: λx.A[x], pair: <a, b>, inr: inr x , inl: inl x, add: n + m, natural_number: $n
FDL editor aliases : collect_accum collect_accum

Latex:
collect\_accum(x.num[x];init;a,v.f[a; v];a.P[a]) == \mlambda{}s,v. eval n = num[v] in let i,a,w = s in if n <z i then <i, a, inr 0 > if i <z n then if P[f[init; v]] then <n + 1, init, inl f[init; v]> else <n, f[init; v], inr 0 > fi if P[f[a; v]] then <i + 1, init, inl f[a; v]> else <i, f[a; v], inr 0 > fi Date html generated: 2016_05_16-AM-10_11_32 Last ObjectModification: 2013_03_25-PM-01_55_02 Theory : new!event-ordering Home Index