coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Defining merge sort

From: Pierre Casteran <pierre.casteran AT labri.fr>
To: Yevgeniy Makarov <emakarov AT gmail.com>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] Defining merge sort
Date: Thu, 08 Nov 2007 08:07:38 +0100
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Yevgeniy Makarov a �crit :

Concerning Pierre Cast�ran's page for mergesort, it looks a little
strange since the traditional presentation of the algorithm does not
mention trees...

I found this version of mergesort pp 16-17 of the Epigram tutorial, by Conor Mc Bride,
(Exercise : "Structural mergesort").

http://www.e-pig.org/downloads/epigram-notes.pdf

Pierre

[Coq-Club] Defining merge sort, Edsko de Vries
- Re: [Coq-Club] Defining merge sort, Benjamin Werner
- Re: [Coq-Club] Defining merge sort, Julien Forest
  - Re: [Coq-Club] Defining merge sort, Yevgeniy Makarov
    - Re: [Coq-Club] Defining merge sort, Pierre Casteran
    - Re: [Coq-Club] Defining merge sort, Edsko de Vries
  - Re: [Coq-Club] Defining merge sort, Edsko de Vries
    - Re: [Coq-Club] Defining merge sort, Pierre Courtieu
- Re: [Coq-Club] Defining merge sort, frederic . blanqui
- Re: [Coq-Club] Defining merge sort, Matthieu Sozeau
- Re: [Coq-Club] Defining merge sort, Matthieu Sozeau