coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] RE: Functor signature ?

From: "Jevgenijs Sallinens" <Jevgenijs.Sallinens AT btg.org.lv>
To: "'armand AT ie.cnam.fr'" <armand AT ie.cnam.fr>
Cc: "'coq-club AT pauillac.inria.fr'" <coq-club AT pauillac.inria.fr>
Subject: [Coq-Club] RE: Functor signature ?
Date: Fri, 4 Jun 2004 17:13:20 +0300
Encoding: 32 TEXT
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Organization: BTG

Fran?ois Armand wrote:
>What is the rigth way to define functor signature ?

The following script compiled without errors. Possible this helps.
Regards,
Jevgenijs.

Module Type MODULE_PARAMS.

   Parameter param1 param2 : Set.

End MODULE_PARAMS.

Module Type SIG_FONCTEUR.
Declare Module X:MODULE_PARAMS.

   Record E : Set := {
     e1 : X.param1 ;
     e2 : X.param2
   }.

End SIG_FONCTEUR.

(* Implementation... *)

Module MakeSigFonct (X:MODULE_PARAMS) <: SIG_FONCTEUR.
Module X:=X.
   Record E : Set := {
     e1 : X.param1 ;
     e2 : X.param2
   }.
End MakeSigFonct.

[Coq-Club] RE: Functor signature ?, Jevgenijs Sallinens