The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 03/09/2016 08:05 PM, Matthieu Sozeau wrote:
> You are basically asking for putting the pretyper in the tactic monad
> here, so that refine could return multiple successes, right?

I wouldn't restrict it to "refine", if that's what you are implying.  
Actually, I'm not sure what you're implying.:-[   So, maybe this will 
clarify my request:

Class Foo : Type := { value : nat }.

Instance foo_a : Foo := {value := 42}.

Instance foo_b : Foo := {value := 7}.

Goal value = 7.
reflexivity.
Qed.

Goal value = 42.
Fail reflexivity.

Could this second goal be provable as well?

-- Jonathan

> 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