The Coq mailing list

[Jianzhou Zhao <jianzhou AT seas.upenn.edu>]

On Mon, Aug 16, 2010 at 4:23 PM, Evgeny Makarov 
<emakarov AT gmail.com>
 wrote:
> 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.

Thanks. This works.

Extract Inductive nat => "int" [ "0" "succ" ].
Extract Constant plus => "fun a b -> a + b ".
Definition _plus (a b:nat) := plus a b.
Extraction "test" _plus.

I had assumed that "Extract Constant" only works for Axioms.  The
reference also gives such syntax to extract constant:
  Coq < Extract Constant plus "’a" "’b" => " ’a*’b"
What is the symbol before a and b, I tried ' and `, it extracted
  let rec plus -> ’a*’b
I might use a wrong symbol.

If the extracted type, say 'big_int', is not in a module opened by
default, can we also specify OCaml dependencies, adding 'open Big_int'
before extracted code?

>
> Evgeny
>
>



-- 
Jianzhou