The Coq mailing list

[Pierre Letouzey <Pierre.Letouzey AT lri.fr>]

On Tue, 3 Dec 2002, Michel Levy wrote:

> I would like to represent the type list of PolyList by the same type in
> Ocaml.
> The command "Extract Inductive list => bool["[]" "(::)" ]." could not be
> used, because the (::) is not the
> ocaml list constructor. Actually, (::) produces in Ocaml a syntax error.
> How is it possible to represent cons (in Coq) by :: (in Ocaml) ?

For the moment, there is no way to do what you want.
If you define cons as (fun a b -> a :: b), it will not work in patterns...
And (::) was legal (and useful) in caml light, but is now forbiden in
ocaml, for a question of parsing from what I've understood. Some time ago
I submitted a "feature wish" to the caml team. Xavier Leroy told me that
it could be restored, no news since that discussion.

Since you are not the first user to ask for true caml list, I think I will
do that at the whole extraction level. And by the way I while also
translate some other standard coq type to their caml counterparts, like

* boolean
* pairs (I'm getting fed up with (Pair (Pair a b) c) ...)
* options
* sumbool -> bool (or maybe not ?)

Just wait for the next coq version (or look at the coq anonymous cvs
within the next weeks).


Pierre Letouzey.