coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Difference between [Existing Instance] and [Hint Resolve ... : typeclass_instances.]

From: Matthieu Sozeau <mattam AT mattam.org>
To: Jason Gross <jasongross9 AT gmail.com>
Cc: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Difference between [Existing Instance] and [Hint Resolve ... : typeclass_instances.]
Date: Tue, 9 Jul 2013 18:01:31 +0200

Le 9 juil. 2013 à 05:46, Jason Gross <jasongross9 AT gmail.com> a écrit :

http://coq.inria.fr/distrib/8.4/refman/Reference-Manual022.html#hevea_default874 says:

19.6.3 Existing Instance ident

This commands adds an arbitrary constant whose type ends with an applied type class to the instance database. It can be used for redeclaring instances at the end of sections, or declaring structure projections as instances. This is almost equivalent to Hint Resolve ident : typeclass_instances.

How is [Existing Instance] different from [Hint Resolve ... : typeclass_instances.]?

It's just that Existing Instance registers the instance in the instance database additionally.

That one supports Global while hints don't. Also it's gonna be printed by Print Instances Foo.

-- Matthieu

[Coq-Club] Difference between [Existing Instance] and [Hint Resolve ... : typeclass_instances.], Jason Gross, 07/09/2013
- Re: [Coq-Club] Difference between [Existing Instance] and [Hint Resolve ... : typeclass_instances.], Matthieu Sozeau, 07/09/2013