coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Tom Prince <tom.prince AT ualberta.net>
- To: Michael Shulman <mshulman AT ucsd.edu>, Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] typeclass methods in hints
- Date: Tue, 13 Dec 2011 18:44:31 -0700
On Thu, 24 Nov 2011 20:16:52 -0800, Michael Shulman
<mshulman AT ucsd.edu>
wrote:
> 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.
You probably want to add ': typeclass_instances' here.
>
> I am told "some_method cannot be used as a hint". Is there a way to
> do this?
Is is that some_method cannot be used as a hint by *auto*? Certain hints
will only be used by eauto (and typeclasses eauto, which is what is used for
typeclass resolution).
There are a number of other things one can do. The simplest method is to use
':>' instead of ':' when declaring the projection ... this automatically
declares a hint for the projection.
You can also add arbitrary tactics as hints like
Hint Extern 4 (<some-optional-patern>) => <some-tactic> : typeclass_instances.
I have occasionally found it useful to add 'apply <something>' as an
external tactic, because this ignores typeclass transparency
... although I haven't worked out exactly why it is useful.
- Re: [Coq-Club] typeclass methods in hints, Tom Prince
- Re: [Coq-Club] typeclass methods in hints,
Michael Shulman
- Re: [Coq-Club] typeclass methods in hints, Tom Prince
- Re: [Coq-Club] typeclass methods in hints,
Michael Shulman
Archive powered by MhonArc 2.6.16.