The Coq mailing list

[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.''