coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Tutorial on [co]-inductive types

From: Pierre Casteran <pierre.casteran AT labri.fr>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club] Tutorial on [co]-inductive types
Date: Thu, 23 Dec 2004 11:00:49 +0100
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hello,

You can find on http://www.labri.fr/Perso/~casteran/RecTutorial.pdf
(also RecTutorial.ps and RecTutorial.v) an adaptation to Coq V8.0 of
the tutorial on Recursive types by Eduardo Gimenez.

It is still a draft, so comments are welcome.

Pierre

--
Pierre Casteran
(+33) 540006931

----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.

[Coq-Club] Tutorial on [co]-inductive types, Pierre Casteran