Nuprl Definition : bag-drop

bag-drop(eq;bs;a) == case bag-remove1(eq;bs;a) of inl(as) => as | inr(_) => bs

Definitions occuring in Statement : bag-remove1: bag-remove1(eq;bs;a), decide: case b of inl(x) => s[x] | inr(y) => t[y]
Definitions occuring in definition : decide: case b of inl(x) => s[x] | inr(y) => t[y], bag-remove1: bag-remove1(eq;bs;a)
FDL editor aliases : bag-drop

Latex:
bag-drop(eq;bs;a) == case bag-remove1(eq;bs;a) of inl(as) => as | inr($_{}$) =>\000C bs Date html generated: 2016_05_15-PM-08_04_10 Last ObjectModification: 2015_09_23-AM-08_20_48 Theory : bags_2 Home Index