The Coq mailing list

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

I like the idea but something to take into account is that although
the two definitions are equivalent, the elimination policy is slightly
different : the names of the projections of a record are used as a
hint when you destruct an object of that type ; in that case, if you
destruct an hypothesis [A /\ B] defined as a record, you end up with
something like

proj3 : A
proj4 : B
===
...

whereas with the usual definition with anonymous products, the default
Hn names are used. So changing the definition of [and] would break all
scripts where users destruct a conjunction without manually specifying
the names to be introduced, and then use either of these names. I
guess there are many such scripts out there so that may be enough to
get cold feet about such a change.

Stéphane


On Tue, Sep 1, 2009 at 10:16 AM, Cedric 
Auger<Cedric.Auger AT lri.fr>
 wrote:
> That is not a relevant question, rather a remark:
>
> Shouldn't "and" be defined by a record as in:
>
> Set Implicit Arguments.
> Record and (A : Prop) (B : Prop) : Prop :=
> conj
> { proj1 : A;
>  proj2 : B
> }.
>
> So that projections are macro generated? (Same for prod, sigT, ...)
>
> --
> Cédric AUGER
>
> Univ Paris-Sud, Laboratoire LRI, UMR 8623, F-91405, Orsay
>
> --------------------------------------------------------
> 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