The Coq mailing list

[Jevgenijs Sallinens <jevgenijs AT dva.lv>]

Unfortunately modules in Coq are not first-class, so usage of them is limited.
As soon as you will need order, depending on some parameter, you will realize 
that your module is not usable any more (no modules are allowed in sections).
Only way to overcome the problem is to use Coq records, but this came with 
others restrictions (no definitions/notations, etc).
It took me a lot of time to overwrite my development to replace modules with 
records (in cases when first-class objects were needed), so hope this warning 
will help others to save their time.
It would be interesting to get expert's opinion, is it possible (at last in 
theory) to have first-class modules compatible with Coq.
Regards,
Jevgenijs.  

Quoting 
"roconnor AT theorem.ca"
 
<roconnor AT theorem.ca>:

> On Mon, 23 May 2005, Pierre Casteran wrote:
> 
> >   I think that it should be better to develop (in the module framework)
> > a theory of ordered sets (with a compare function) and prove not only
> > the commutativity of min but also associativity, the same for max, ...
> 
> I fully agree with this.  I strongly encourage this sort of modular work.
> 
> To get the ball rolling I have developed a modular framework for min and
> max given a decidable total order.  A dualizing module functor is created,
> and max and its theory is defined to the dual of min.  This means all the
> theory of min is reused in the theory of max.
> 
> Anyone is free to take this and add/improve upon it.
> 
> -- 
> 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.''




-------------------------------------------------
This mail sent through IMP: http://webmail.dva.lv/