coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Extracting integers from Coq to OCaml

From: Evgeny Makarov <emakarov AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Extracting integers from Coq to OCaml
Date: Tue, 17 Aug 2010 00:23:31 +0400
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :content-type:content-transfer-encoding; b=ZDXEcUpYnw5hcxZtuOnHtcZpHk8w4XSqIhy9vtNeSThf7hfDXXUj+83lUtXA4G/nDJ VqCmdVhr3wFfP8rtDPOBajtx2E5V4mR7elYnr3cg2vaLiGI5Ph5Xmg30PoxVAwEHpgNu J6ZS1MV6Q0qg9CAseTVWIJhtnYpIo09t/l64U=

Jianzhou,

> I think Coq extraction
> (http://coq.inria.fr/refman/Reference-Manual027.html#toc139) only
> allows to realize inductive Coq types into inductive OCaml types. �But
> OCaml's int or big_bit is only primitive.

The Reference Manual section 21.2.4 (at least after trunk 13264) has
an example of extracting the inductive Coq type nat to OCaml type int.
The command is "Extract Inductive". You can also probably use "Extract
Constant" to map functions on a Coq type into built-in OCaml
functions.

Evgeny

[Coq-Club] Extracting integers from Coq to OCaml, Jianzhou Zhao
- Re: [Coq-Club] Extracting integers from Coq to OCaml, Evgeny Makarov
  - Re: [Coq-Club] Extracting integers from Coq to OCaml, Jianzhou Zhao
    - Re: [Coq-Club] Extracting integers from Coq to OCaml, Jianzhou Zhao
    - Re: [Coq-Club] Extracting integers from Coq to OCaml, Pierre Letouzey
      - Re: [Coq-Club] Extracting integers from Coq to OCaml, Jianzhou Zhao