Ssreflect Users Discussion List

[Georges Gonthier <>]

  Actually, the first two files you mention do not develop the theory of 
permutations, but define equality up to permutation (i.e., multiset equality) 
on lists; in the ssreflect library this is a (small) part of the sequence 
library (seq.v). I suppose the first two might be unified; the ssreflect one 
exploits the decidable equality infrastructure in the combinatorial to get 
simpler definitions that are easier to compose (though they might still be 
linked to the former). A decent theory of permutations requires a fair amount 
of background group theory, so if you require that you'll probably have to 
buy into the ssreflect library.

Georges

-----Original Message-----
From:  [] On Behalf Of 
Bas Spitters
Sent: 16 November 2009 13:21
To: Ssreflect-mailinglist; Coq Club
Subject: Permutations

There are at least three libraries of permutations:
 http://coq.inria.fr/contribs/Huffman.Permutation.html
 http://coq.inria.fr/library/Coq.Sorting.Permutation.html
 Ssreflect's perm.v

Are there others?
Is there any initiative to unify them?

Thanks,

Bas