The Coq mailing list

[anoun AT labri.fr]

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.