coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] representation of Coq list in Ocaml

From: Francois-Rene Rideau <fare AT tunes.org>
To: Pierre Letouzey <Pierre.Letouzey AT lri.fr>
Cc: Michel Levy <michel.levy AT imag.fr>, coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] representation of Coq list in Ocaml
Date: Tue, 3 Dec 2002 19:37:43 +0100
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

On Tue, Dec 03, 2002 at 07:16:01PM +0100, Pierre Letouzey wrote:
>> I would like to represent the type list of PolyList by the same type 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...
Just my .2 mg of gold, but it looks like a job for camlp4...

[ Fran�ois-Ren� �VB Rideau | Reflection&Cybernethics | http://fare.tunes.org ;]
[ TUNES project for a Free Reflective Computing System | http://tunes.org ;]
Is eating the flesh around one's nails to be considered as anthropophagy,
and does it qualify one for eternal damnation to burn in hell?

[Coq-Club] representation of Coq list in Ocaml, Michel Levy
- Re: [Coq-Club] representation of Coq list in Ocaml, Pierre Letouzey
  - Re: [Coq-Club] representation of Coq list in Ocaml, Francois-Rene Rideau