Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] typeclass methods in hints

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] typeclass methods in hints


chronological Thread 
  • From: Damien Pous <Damien.Pous AT inria.fr>
  • Cc: Coq Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] typeclass methods in hints
  • Date: Sat, 26 Nov 2011 18:49:33 +0100

Hi,
I support this feature request...
As Michael said, declaring the hint with @ is often not satisfactory
(when possible), since the maximally implicit arguments should usually
be filled by typeclass resolution rather than by (e)auto.
Best,
Damien


2011/11/25 Michael Shulman 
<mshulman AT ucsd.edu>:
> Is it possible to declare a typeclass method as a hint?  When I say
>
> Hint Resolve some_method.
>
> if no instances have yet been declared, I get a "cannot infer implicit
> parameter" error.  If some instances have been declared, then
> apparently only the method applied to the first such instance is
> declared as a hint.  I can specify which instance I want with
>
> Hint Resolve (@some_method some_instance).
>
> but I want the hint to apply to *all* instances.  However, if I write
>
> Hint Resolve @some_method.
>
> I am told "some_method cannot be used as a hint".  Is there a way to do 
> this?
>
> Thanks,
> Mike
>




Archive powered by MhonArc 2.6.16.

Top of Page