Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] [Type Classes]: avoid duplication of instances

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] [Type Classes]: avoid duplication of instances


chronological Thread 
  • 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




Archive powered by MhonArc 2.6.16.

Top of Page