coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] multiple typeclass instance question

From: Vadim Zaliva <vzaliva AT cmu.edu>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] multiple typeclass instance question
Date: Wed, 9 Mar 2016 15:49:41 -0800
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=vadim.zaliva AT west.cmu.edu; spf=None smtp.mailfrom=vadim.zaliva AT west.cmu.edu; spf=None smtp.helo=postmaster AT mail-wm0-f46.google.com
Ironport-phdr: 9a23:mZR52B8oOPZ6aP9uRHKM819IXTAuvvDOBiVQ1KB90OscTK2v8tzYMVDF4r011RmSDdqdu60P0rCempujcFJDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXsq3G/pQQfBg/4fVIsYL+lRciC0I/ujaibwN76XUZhvHKFe7R8LRG7/036l/I9ps9cEJs30QbDuXBSeu5blitCLFOXmAvgtI/rpMYwu3cYh/V0/MlZFK7+Yq4QTLpCDT1gPXpmytfssEz9RAeO4zMuW2EXjBMAVxbX5RX7QJ7ZuS7n8OdxxX/JboXNUbkoVGH6vO9QQxjyhXJfOg==

How about something like this:

Instance Zmult_op : monoid_binop Z | 1 := Zmult.

Instance Zplus_op : monoid_binop Z | 2 := Zplus.

(from http://www.labri.fr/perso/casteran/CoqArt/TypeClassesTut/typeclassestut.pdf )

Vadim

CMU ECE PhD candidate

Mobile: +1(510)220-1060

Skype: vzaliva

On Wed, Mar 9, 2016 at 1:38 PM, Jonathan Leivent <jonikelee AT gmail.com> wrote:

Suppose one has multiple typeclass instances of the same exact class (same exact parameterization). Is there a way to get to more of them other than just the most recently declared one with the highest priority?

-- Jonathan

[Coq-Club] multiple typeclass instance question, Jonathan Leivent, 03/09/2016
- Re: [Coq-Club] multiple typeclass instance question, Vadim Zaliva, 03/10/2016
  - Re: [Coq-Club] multiple typeclass instance question, Jonathan Leivent, 03/10/2016
    - Re: [Coq-Club] multiple typeclass instance question, Matthieu Sozeau, 03/10/2016
      - Re: [Coq-Club] multiple typeclass instance question, Jonathan Leivent, 03/10/2016
        
        Re: [Coq-Club] multiple typeclass instance question, Jonathan Leivent, 03/10/2016
        
        Re: [Coq-Club] multiple typeclass instance question, Jason Gross, 03/10/2016
        
        Re: [Coq-Club] multiple typeclass instance question, Jonathan Leivent, 03/10/2016
        Re: [Coq-Club] multiple typeclass instance question, Jason Gross, 03/10/2016
        Re: [Coq-Club] multiple typeclass instance question, Jonathan Leivent, 03/10/2016
        Re: [Coq-Club] multiple typeclass instance question, Jonathan Leivent, 03/10/2016
        
        Re: [Coq-Club] multiple typeclass instance question, Jason Gross, 03/10/2016