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: Guilhem Moulin <guilhem.moulin AT ens-lyon.org>
  • To: Ryan Rusich <rusichr AT cs.ucr.edu>
  • Cc: coq-club <coq-club AT pauillac.inria.fr>
  • Subject: Re: [Coq-Club] extraction of natural language from proofs
  • Date: Fri, 5 Jun 2009 17:24:00 +0200
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=sender:date:from:to:cc:subject:message-id:mail-followup-to :references:mime-version:content-type:content-disposition :in-reply-to:user-agent; b=JoCVaEi6yc8azpoYd+6CBbdkou0Ubd9pwwB98pYWqNq/g8RDA3xQiqXB0KzaLTCo2R Mv5S8y0k4QUPEfr2ljtp9JyAeSgQ9jUZ197GpSje5K58d9KWiB2ilYpNIds4PbE/Rz+0 Q7JjnW2xB4aGvgdVfwJKkM3djHtEutOfUH2LQ=
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
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

Attachment: signature.asc
Description: Digital signature


Archive powered by MhonArc 2.6.16.

Top of Page