Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
  • 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




Archive powered by MHonArc 2.6.18.

Top of Page