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.]?
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
Archive powered by MHonArc 2.6.18.