The Coq mailing list

[Andrej Bauer <andrej.bauer AT andrej.com>]

> Class Enumeration (A:Type) : Type :=
> | elements : list A.
>
> Implicit Arguments elements [[Enumeration]].
>
> Definition finite_card (A:Type) `{Enumeration A} : nat :=
>   length (elements A).
>
> (* I'm not sure whether it's better to require the enumeration be
>    exhaustive and have no duplications, before allowing the application
>    of this notation. *)
> Notation "# A" := (finite_card A) (at level 0).

If your intention is to represent finite sets as Enumerations, then
finite_card is not well-defined precisely for the reason you notice:
an enumeration may list some elements several times. Thus the
enumerations [1,2,1] and [1,2] both name the same set, but they have
different lengths.

Sets whose elements can be enumerated (with repetition) by finite
lists are called Kuratowski finite. There is no well-defined
cardinality function for Kuratowski finite sets. In fact, having the
cardinality function for Kuratowski finite subsets of some given set A
is equivalent to A having decidable equality (to decide x = y compute
the cardinality of {x, y}, conversly to compute the cardinality weed
out duplicates in an enumeration, using decidable equality).

With kind regards,

Andrej