The Coq mailing list

[St�phane Lescuyer <stephane.lescuyer AT inria.fr>]

I'm not the author of this library but it seems to me that the carrier
is required in the definition of the partial order because it must be
non-empty. The alternative would be to have the carrier as an argument
to the PO type :

 Record PO (C : Ensemble U) : Type := Definition_of_PO
    {Rel_of : Relation U;
      PO_cond1 : Inhabited U C;
      PO_cond2 : Order U Rel_of }.

However, it is slightly more convenient to have the carrier come with
the partial order rather than being an argument of it. For instance
see the definition of CPO's in the same library : one only has to
assume a partial order, and can then refer to the carrier in the
definitions. It may be just a matter of style and taste, though :)

Stéphane L.

On Sun, Feb 22, 2009 at 6:03 PM, Samuel E. Moelius III
<moelius AT cis.udel.edu>
 wrote:
> In PO in Coq.Sets.Partial_Order, what is the rationale for having the
> ``Carrier_of'' field?
>
> For example, is there some application that is made easier by its presence?
>
> Thanks in advance.
>
> Sam
>
> --------------------------------------------------------
> Bug reports: http://logical.saclay.inria.fr/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
>



-- 
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06