The Coq mailing list

[Elie Soubiran <soubiran AT lix.polytechnique.fr>]

Hello,

If you are using coq 8.1 you should do as follow:

Module Type SIG.

Parameter t : T.
Parameter foo : t -> Prop.

End SIG.

Module F (X:SIG2) : SIG with Definition t := X.t.

Definition t : T := P.t.
Definition foo : t -> Prop := ...

End F.

Or if you are using 8.2 or trunk you can keep your type SIG but use it
like this:

Module F (X:SIG2) : SIG X.
....


Elie


On Fri, Jan 30, 2009 at 10:15 PM, M. Scott Doerrie 
<mdoerri AT cs.jhu.edu>
 wrote:
> I have defined a ModuleType functor and a Module functor somewhat as
> follows.
>
> For discussion assume SIG2 is a Module Type.
>
> Module Type SIG (P: SIG2).
>
> Parameter foo : P.t -> Prop.
>
> End SIG.
>
>
> Module Impl (P:SIG2).
>
> Definition foo (P:t) : Prop :=  (* implementation *).
>
> End Impl
>
>
> I can't determine how to declare that Impl is of type SIG?  Use of <: and :
> operators produce syntactic error messages.  I'm sure this is a simple
> example, but I am confused by what I thought was straightforward to express.
>
> Scott Doerrie
>
> --------------------------------------------------------
> Bug reports: http://logical.futurs.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>         http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>