coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] How to generate sequence calculus from coq code?

From: tumenjargal tsagaan <delgiika AT yahoo.de>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club] How to generate sequence calculus from coq code?
Date: Mon, 17 Aug 2009 13:34:17 +0000 (GMT)
Domainkey-signature: a=rsa-sha1; q=dns; c=nofws; s=s1024; d=yahoo.de; h=Message-ID:X-YMail-OSG:Received:X-Mailer:Date:From:Subject:To:MIME-Version:Content-Type; b=J00VRSUUyfsmJqNeznNmxpNk4rDCIrxSV96owWSA/Vwnp10cCYLO7qtmF089gIdjBBgIcvOiikvSHhiPbJH3XLrJzAJErXvA2DKaWwa1Q3OMd/XhVxnjjqcKOsPVbFi30XKHo39KXPeidlnRKtqRKyAgFy89KaKqcxxtavahaHg=;
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hi All,

I wanted to rewrite coq-code in a sequence form.
Is there any automated tool for this purpose?

even better is it if possible in a tex format.

Thank you a lot.

Best regards,

Tumee.

[Coq-Club] How to generate sequence calculus from coq code?, tumenjargal tsagaan
- Re: [Coq-Club] How to generate sequence calculus from coq code?, Yves Bertot
- Re: [Coq-Club] How to generate sequence calculus from coq code?, Adam Chlipala
  - Re: [Coq-Club] How to generate sequence calculus from coq code?, Cedric Auger