The Coq mailing list

[Cedric Auger <Cedric.Auger AT lri.fr>]

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