The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

I meant something more like this:

Class Foo : Type.

Instance foo_a : Foo.

Instance foo_b : Foo.

Goal True.
try (refine (let x := _ : Foo in _);
      let y := eval unfold x in x in idtac y; fail).

The above prints only foo_b, because that is the most recent definition 
(since their costs are the same).  Using costs, one can make it so that 
foo_a is printed, but not foo_b.  But, is there a way to have something 
print both foo_a and foo_b?

-- Jonathan

On 03/09/2016 06:49 PM, Vadim Zaliva wrote:
> 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