The Coq mailing list

[frederic.blanqui AT loria.fr]

On Wed, 7 Nov 2007, Edsko de Vries wrote:

> 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?

see for instance the multiset modules of the CoLoR library on 
http://color.loria.fr/.