The Coq mailing list

[Edsko de Vries <devriese AT cs.tcd.ie>]

Hi,

Is there an implementation of multisets in Coq which has the property
that for two multisets M1 and M2, union M1 M2 = union M2 M1 (as in the
Multiset implementation in the standard library), but is "concrete" in
the sense that it supports an operation elems :: Multiset A -> List A?

Thanks,

Edsko