The Coq mailing list

[Stefan Karrmann <sk AT mathematik.uni-ulm.de>]

Hi,

have you read documentation chapter 18 ('Extraction of programs in
Objective Caml and Haskell', cf.
<http://pauillac.inria.fr/coq/doc8/Reference-Manual021.html>)?

Or try:

   Extraction "first" function_name.

Yevgeniy Makarov (Fri, Feb 18, 2005 at 08:36:33PM -0500):
> I am interested in using Coq for program extraction from classical
> proofs. Coq seems suitable for this because it produces nice proof
> terms, which are almost programs. So I hope to prove theorems in Coq,
> take proof terms and use them by my own programs to replace the
> classical rule NNPP by call/cc, eliminate computationally irrelevant
> information, normalize, and so on (currently I have a normalizer
> written in Scheme). It is quite possible to parse proof terms that are
> displayed by Print command, but I am wondering if there is a still
> easier way, namely, if I can get an access to the proof term's inner
> representation.
> 
> Thank you,
> Yevgeniy

Regards,
-- 
Stefan Karrmann