coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: St�phane Lescuyer <stephane.lescuyer AT polytechnique.org>
- To: Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org>
- Cc: Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] [Type Classes]: avoid duplication of instances
- Date: Fri, 1 Oct 2010 18:48:37 +0200
- Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:date :x-google-sender-auth:message-id:subject:from:to:cc:content-type :content-transfer-encoding; b=F65jlJKNx8j+O9LIb5AWYTl6VVJLpPzDQtOROdQwNlmRqyNxgIxggECS++9LgvFF41 hfYkGOvKd49/LPq+VRoswWTbpgw+e4hb0jCylGMW83SnrMS1z+9yylZlf8VSZ/GCLdiA Ajkpsb19MxN3q186AU726CEGbnpiQ03zClMyw=
Hi,
How did you define your module for positives with signature TREE exactly ?
If you go like this:
<<<
Module BinPosTree <: TREE.
Definition elt := positive.
Definition EqDec_elt := EqDec_positive.
End
>>>
where I suppose EqDec_positive is a preexisting instance for positive,
everything will work fine (you don't define a new instance per se,
it's just a regular definition, and the signature checking <: TREE
only checks the types of the definitions, not the fact that it is
declared as in instance.
You can check with "Print Instances EqDec" that only EqDec_positive is
available after defining this module, but you can use it on elements
of type BinPosTree.t:
<<<
Goal forall (x y : BinPosTree.elt), if x == y then x = y else True.
...
>>>
If on the contrary you do something like this:
<<<
Module BinPosTree <: TREE.
Definition elt := positive.
Instances EqDec_elt : EqDec positive.
exact EqDec_positive.
Defined.
End
>>>
this is a new instance definition and then you will experience the
issues you described.
Hope this helps,
Stéphane
--
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06
- [Coq-Club] [Type Classes]: avoid duplication of instances, Alexandre Pilkiewicz
- Re: [Coq-Club] [Type Classes]: avoid duplication of instances, Stéphane Lescuyer
- Re: [Coq-Club] [Type Classes]: avoid duplication of instances,
Alexandre Pilkiewicz
- Re: [Coq-Club] [Type Classes]: avoid duplication of instances,
Stéphane Lescuyer
- Re: [Coq-Club] [Type Classes]: avoid duplication of instances, Alexandre Pilkiewicz
- Re: [Coq-Club] [Type Classes]: avoid duplication of instances,
Aaron Bohannon
- Re: [Coq-Club] [Type Classes]: avoid duplication of instances,
Stéphane Lescuyer
- Re: [Coq-Club] [Type Classes]: avoid duplication of instances,
Aaron Bohannon
- Re: [Coq-Club] [Type Classes]: avoid duplication of instances, Stéphane Lescuyer
- Re: [Coq-Club] [Type Classes]: avoid duplication of instances, Aaron Bohannon
- Re: [Coq-Club] [Type Classes]: avoid duplication of instances,
Aaron Bohannon
- Re: [Coq-Club] [Type Classes]: avoid duplication of instances,
Aaron Bohannon
- Re: [Coq-Club] [Type Classes]: avoid duplication of instances, Stéphane Lescuyer
- Re: [Coq-Club] [Type Classes]: avoid duplication of instances,
Stéphane Lescuyer
- Re: [Coq-Club] [Type Classes]: avoid duplication of instances,
Stéphane Lescuyer
- Re: [Coq-Club] [Type Classes]: avoid duplication of instances,
Alexandre Pilkiewicz
- Re: [Coq-Club] [Type Classes]: avoid duplication of instances, Stéphane Lescuyer
Archive powered by MhonArc 2.6.16.