Nuprl Definition : consensus-accum
consensus-accum(s;e) ==
let i,est,knw = s in
case e
of inl(x) =>
<i + 1, est, knw>
| inr(x) =>
case x of inl(v) => <i, est ⊕ i : v, knw> | inr(k) => let b,i',z = k in <i, est, b : <i', z> ⊕ knw>
Definitions occuring in Statement :
fpf-single: x : v,
fpf-join: f ⊕ g,
id-deq: IdDeq,
int-deq: IntDeq,
spreadn: spread3,
pair: <a, b>,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
add: n + m,
natural_number: $n
FDL editor aliases :
consensus-accum
consensus-accum(s;e) ==
let i,est,knw = s in
case e
of inl(x) =>
<i + 1, est, knw>
| inr(x) =>
case x of inl(v) => <i, est \moplus{} i : v, knw> | inr(k) => let b,i',z = k in <i, est, b : <i', z> \moplus{} kn\000Cw>
Date html generated:
2015_07_17-AM-11_44_30
Last ObjectModification:
2012_02_25-AM-11_47_35
Home
Index