Nuprl Definition : bag_all
bag_all(b;f) == bag-accum(a,x.a ∧b f[x];tt;b)
Definitions occuring in Statement :
bag-accum: bag-accum(v,x.f[v; x];init;bs),
band: p ∧b q,
btrue: tt,
so_apply: x[s]
Definitions occuring in definition :
bag-accum: bag-accum(v,x.f[v; x];init;bs),
band: p ∧b q,
so_apply: x[s],
btrue: tt
FDL editor aliases :
bag_all
Latex:
bag\_all(b;f) == bag-accum(a,x.a \mwedge{}\msubb{} f[x];tt;b)
Date html generated:
2016_05_15-PM-02_34_30
Last ObjectModification:
2015_09_23-AM-07_39_39
Theory : bags
Home
Index