coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] Question about Modules., roconnor
- Re: [Coq-Club] Question about Modules.,
anoun
- Re: [Coq-Club] Question about Modules., Robert Dockins
- Re: [Coq-Club] Question about Modules., Pierre Casteran
- Re: [Coq-Club] Question about Modules., Robert Dockins
- Re: [Coq-Club] Question about Modules., Stefan Karrmann
- Re: [Coq-Club] Question about Modules.,
Carlos.SIMPSON
- Re: [Coq-Club] Question about Modules., Hugo Herbelin
- Re: [Coq-Club] Question about Modules.,
anoun
Archive powered by MhonArc 2.6.16.