The Coq mailing list

["M. Scott Doerrie" <mdoerri AT cs.jhu.edu>]

I'm using an 8.1 derivitive, but had been trying to use the 8.2 syntax.  
Thanks for the clarification.

Scott Doerrie

Elie Soubiran wrote:
> 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
> >
> >     
>
> --------------------------------------------------------
> 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
>