coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Ryan Rusich <rusichr AT cs.ucr.edu>
- To: coq-club <coq-club AT pauillac.inria.fr>
- Subject: [Coq-Club] extraction of natural language from proofs
- Date: Fri, 5 Jun 2009 07:57:31 -0700
- Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:from:date:x-google-sender-auth:message-id :subject:to:content-type; b=hrueOpMqlx+wWkLpg0edq98gTYX2eMJ8lTfpElcA69yUn0c0tIfaPfyx1yBh2hC0+u S79cOlIGlubRDZeEfLwPK3NpKJ+38iK88roIxXP2uYPkw+rPeUWFt7/R/t0nXAct/hii RE5eRuv8YMnFCnJn7u6HYbBWkQHyQTrIajlXA=
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
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
Ryan
- [Coq-Club] extraction of natural language from proofs, Ryan Rusich
- Re: [Coq-Club] extraction of natural language from proofs,
Guilhem Moulin
- Re: [Coq-Club] extraction of natural language from proofs, Lukasz Stafiniak
- Re: [Coq-Club] extraction of natural language from proofs, Ryan Rusich
- Re: [Coq-Club] extraction of natural language from proofs, CHA Reeseo
- Re: [Coq-Club] extraction of natural language from proofs, Yves Bertot
- Re: [Coq-Club] extraction of natural language from proofs,
Guilhem Moulin
Archive powered by MhonArc 2.6.16.