The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

You are basically asking for putting the pretyper in the tactic monad

here, so that refine could return multiple successes, right? 

I think Arnaud had some ideas about this.

-- Matthieu

On Thu, Mar 10, 2016 at 1:08 AM Jonathan Leivent <jonikelee AT gmail.com> wrote:

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
>>
>>