The Coq mailing list

[Thery Laurent <thery AT ns.di.univaq.it>]

Hi,

On Wed, 28 Jan 2004, Iris Loeb wrote:

> Is there any development of permutations (of natural numbers) other than 
> "Permutation" in the Standard Library?
> 

if you are looking inside the development of Hufman algorithm 

ftp://ftp-sop.inria.fr/lemme/Laurent.Thery/Huffman/index.html

In Permutation.v

ftp://ftp-sop.inria.fr/lemme/Laurent.Thery/Huffman/Permutation.html
 
there is an alternative and more direct definition of permutations 
(as a sequence of adjacent transpositions) along with quite a complete set 
of proved properties


Hope this helps

--
Laurent Théry