The Coq mailing list

[AUGER C�dric <Cedric.Auger AT lri.fr>]

I had some problem with Extraction function,
Records are known to be non-recursive in Coq,
but in CaML, we can use recursive records such as:

type foo = Foo | Foobar of bar
and bar = {x : foo; y : bool}

this type is "inductively" correct, as "proven" in the Coq term:

Require Import Bool.

Inductive foo : Set :=
| Foo : foo
| Foobar : bar -> a
with bar : Set :=
| Build_bidule : foo -> bool -> bar
.

but the extracted type is not a Record (hopefully, since
we didn't provided the field names), and I want it to be
a Record, so a mechanism such as:

Require Import Bool.

Inductive foo : Set :=
| Foo : foo
| Foobar : bar -> a
with bar : Set :=
| Build_bidule : foo -> bool -> bar
as Record [ x y ]
.
would be usefull to change easily the status of an Inductive type

(maybe not as readable as

Inductive foo : Set :=
| Foo : foo
| Foobar : bar -> a
with bar : Set :=
| Build_bidule : {x : foo; y : bool} as Record
.
or so...)

I do not really know what problems can be encountered;
I believe this is just a flag to set in Coq to be extracted
as record type.

For other languages, such as Haskell, as I don't know them,
I don't know if it is problematic.

Am I wrong and have to do without those Record or could it
be implemented and added to Coq features?

-- 
Cédric AUGER

Univ Paris-Sud, Laboratoire LRI, UMR 8623, F-91405, Orsay