Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] extraction of natural language from proofs

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] extraction of natural language from proofs


chronological Thread 
  • From: Ryan Rusich <rusichr AT cs.ucr.edu>
  • To: Guilhem Moulin <guilhem.moulin AT ens-lyon.org>, Ryan Rusich <rusichr AT cs.ucr.edu>, coq-club <coq-club AT pauillac.inria.fr>
  • Subject: Re: [Coq-Club] extraction of natural language from proofs
  • Date: Fri, 5 Jun 2009 09:45:00 -0700
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:from:date :x-google-sender-auth:message-id:subject:to:content-type; b=ao3Dub3uqPwqrA2GTSDHf/QQ0cgCTdouU1fR0Tl9CXOQx+ZZ4uhv6DbI2tY5xuYUjO rY+k40xZZndKATH0FwQkOuEk5CXkmBOHKZf0N2hMi9lm9CxrQT9cvG7odB3/emslCfZs Bma75LFkfK4l47PZGkTUAOr3H6419Xft1UnH8=
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Dear Guilhem, 

Thanks for your quick reply. 

The current Coq reference manual http://coq.inria.fr/coq/distrib/current/refman/  contains a section entitled "Credits: addendum for version 6.1"  (Christine Paulin, Nov. 18th 1996), which states that "Yann Coscoy designed a command which explains a proof term using natural language [that has been] integrated to the Coqsystem by Hugo Herbelin."  I'm  trying (so far unsuccessfully) to find the name of and documentation for that command.

Ryan


On Fri, Jun 5, 2009 at 8:24 AM, Guilhem Moulin <guilhem.moulin AT ens-lyon.org> wrote:
I'm not sure that is what you looking for, but here is the relevant
chapter of the reference manual:
http://www.lix.polytechnique.fr/coq/distrib/v8.2/refman/Reference-Manual027.html

You can also take a look on chapters 10-11 of the Coq'Art:
http://www.labri.fr/perso/casteran/CoqArt/index.html

On Fri, 05 Jun 2009 at 07:57:31 -0700, Ryan Rusich wrote:
> Dear All, Can anyone point me in the direction of the documentation for
> extracting natural language from proofs using Coq? I read that it was
> included in Coq from version 6.2 on, but have run into some difficulty
> identifying the name of the command, and the location documentation
> pertaining to it on the Coq website.
> Thank you,
> Ryan

-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.9 (GNU/Linux)

iEYEARECAAYFAkopOJAACgkQ42JSn70VGn1lRgCfe537RXPe/jP+uzbtFSGRKrgH
y2kAnj0JJxD6UcxxSNdstZ7JcCEtiA0l
=/K9o
-----END PGP SIGNATURE-----




--
Cheers, Ryan



Archive powered by MhonArc 2.6.16.

Top of Page