Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Question about Modules.

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Question about Modules.


chronological Thread 
  • From: Robert Dockins <robdockins AT fastmail.fm>
  • To: anoun AT labri.fr
  • Cc: Coq Club <coq-club AT pauillac.inria.fr>
  • Subject: Re: [Coq-Club] Question about Modules.
  • Date: Sat, 12 Mar 2005 16:31:56 -0500
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

In the declaration for Module DualSpace you have 'VectorSpace with
Module F:=G'  and then 'Module F:=G' again in the body.  Why is that
necessary?

More generally, is there a good place to learn how to use Coq modules?
The documentation is less than helpful, and I haven't got the cash for
Coq'Art just now.

On Sat, 2005-03-12 at 19:52 +0100, 
anoun AT labri.fr
 wrote:
> Hi Russel,
> The problem comes from using type functors, we can replace that by 
> declaring a
> Module F inside the signature VectorSpace like the following:
> 
> Module Type Field.
> Parameter K:Set.
> Parameter plus: K -> K -> K.
> (*...*)
> End Field.
> 
> Module Type VectorSpace.
> Declare Module F:Field.
> Parameter V:Set.
> Parameter plus: V -> V -> V.
> Parameter scale: F.K -> V -> V.
> (*...*)
> End VectorSpace.
> 
> Module DualSpace (G:Field) (V:VectorSpace with Module F:=G) : VectorSpace 
> with
> Module F:=G.
> 
> Module F:=G.
> Definition V := {f:V.V->F.K | linear f}
> (*...*)
> End DualSpace.
> 
> 
> Regards,
> Houda
> 
> 
> 
> Quoting 
> roconnor AT theorem.ca:
> 
> > I am trying to understand Coq's Module system.  I want to do something
> > analogous to having a Module Type for fields.  Having a Module Type for
> > vector spaces with a field parameter, and having a Fuctor taking a vector
> > space to the dual vector space.
> >
> > Module Type Field.
> > Parameter K:Set.
> > Parameter plus: K -> K -> K.
> > (*...*)
> > End Field.
> >
> > Module Type VectorSpace (F:Field).
> > Parameter V:Set.
> > Parameter plus: V -> V -> V.
> > Parameter scale: F.K -> V -> V.
> > (*...*)
> > End VectorSpace.
> >
> > Module DualSpace (F:Field) (V:VectorSpace F) : VectorSpace F.
> > Definition V := {f:V.V->F.K | linear f}
> > (*...*)
> > End DualSpace.
> >
> > Coq complains at my definition of DualSpace.  It is entirely possible I
> > have no idea what I am doing.
> >
> > --
> > Russell O'Connor                                      <http://r6.ca/>
> > ``All talk about `theft,''' the general counsel of the American 
> > Graphophone
> > Company wrote, ``is the merest claptrap, for there exists no property in
> > ideas musical, literary or artistic, except as defined by statute.''
> > --------------------------------------------------------
> > Bug reports: http://coq.inria.fr/bin/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
> >
> 
> 
> 
> 
> ----------------------------------------------------------------
> This message was sent using IMP, the Internet Messaging Program.
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/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




Archive powered by MhonArc 2.6.16.

Top of Page