coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Insertion sorting on lists ... in the Coq standard library or where else?

From: Catalin Hritcu <catalin.hritcu AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Insertion sorting on lists ... in the Coq standard library or where else?
Date: Tue, 30 Mar 2010 18:34:32 +0200
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:date:message-id:subject:from:to:content-type; b=LYkRec+DVRIyIXue7tTgJE8eKxFdAcJZQ2QAUromUzbuOgYf9DfYpqnWPkrRKqd4SM 4QLLRlBi8vqStw70cpER3R12GbB9dYQEqKotfz6MnCwrDKgjMqxa9HUG/U10zIC05V5B XTuCKqi+UWsldurV6BUHk822nVKDsqVYlwIiA=

Hello,

I have a very basic question: is there any implementation of insertion
sorting on lists in the Coq standard library? The cocorico wiki
suggests there would be one
(http://coq.inria.fr/cocorico/FormalizedAndVerified), but I couldn't
find it. All I could find was the specification of what it means to be
sorted in http://coq.inria.fr/library/Coq.Sorting.Sorting.html

If it's not really in the standard library can somebody point me to
where I can find it?

Thanks a lot,
Catalin

[Coq-Club] Insertion sorting on lists ... in the Coq standard library or where else?, Catalin Hritcu
- Re: [Coq-Club] Insertion sorting on lists ... in the Coq standard library or where else?, Matthew Brecknell
  - Re: [Coq-Club] Insertion sorting on lists ... in the Coq standard library or where else?, Catalin Hritcu