coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Jason Gross <jasongross9 AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] Difference between [Existing Instance] and [Hint Resolve ... : typeclass_instances.]
Date: Mon, 8 Jul 2013 23:46:45 -0400

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.]?

Thanks,

Jason

[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