coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "Carlos.SIMPSON" <carlos AT math.unice.fr>
- To: coq-club AT pauillac.inria.fr
- Subject: coercions
- Date: Thu, 03 May 2001 16:14:02 -0100
Hi.
I was looking at the coercion mechanism and have a small question.
There seems
to be something that is not explained in the reference manual,
namely the meaning of the first optional coercion symbol
in a Record type. For example in the Setoids.v file
(e.g. in Saibi's category theory files), it starts with :
Structure >Setoid : Type :=
{Carrier :> Type;
Equal : (Relation Carrier);
Prf_equiv :> (Equivalence Equal)}.
While the second and third symbols > are explained in the reference
manual, the first one (i. e. >Setoid) isnt. I tried writing this type of thing
in a test but got back the message ``Build_myrecordtype doesnt
satisfy the uniform inheritance condition''. Can someone explain what
is going on, for example in the case of Setoids above?
Does it have something to do with the implicit arguments, i.e. is it
that when `implicit arguments on' allows the Build_ to use only one argument
then you can turn it into a coercion or something like that?
Another question: why wasn't Equal :> ... declared as a coercion?
is there any disadvantage to declaring a coercion?
Thanks
---Carlos
- coercions, Carlos.SIMPSON
Archive powered by MhonArc 2.6.16.