The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

If I remember correctly, extraction to Haskell does not produce modules (mainly because there is no module Type equivalent in Haskell), so if you do not really care of the target language, you might exploit it.

2014-02-21 14:05 GMT+01:00 Rui Baptista <rpgcbaptista AT gmail.com>:

Hi,

Is [Parameter Inline] what you're looking for?

Regards, Rui Baptista

On Fri, Feb 21, 2014 at 12:56 PM, Kirill Taran <kirill.t256 AT gmail.com> wrote:

Hello.

Is it possible to configure extraction such way that all modules will be eliminated from extracted code and parameters of them will be replaced with explicit extra arguments to functions?

E.g. this:

Module Type T.

Parameter P : Set.

End M.

(* In one file: *)

Module N := T nat. Import N.

Definition f : P := 1.
(* In other file: *)

Module B := T bool. Import N.

Definition f : P := true.

must become this:

(* In one file: *)

Definition f : nat := 1.
(* In other file: *)

Definition f : bool := true.

Sincerely,
Kirill Taran

--
.../Sedrikov\...