Stream: Coq users

Topic: Hole ineligible for typeclass resolution?


view this post on Zulip Shea Levy (Nov 04 2020 at 02:16):

I have a habit of leaving holes and letting PG tell me the type needed to fill each one by one, but I'm dealing with a typeclass heavy domain right now and most of the holes lead to very long/indefinite spinning looking for an instance and then an error on the whole term, not the "next" hole. Is there a way to tell coq not to try using typeclass resolution for some hole?

view this post on Zulip Paolo Giarrusso (Nov 04 2020 at 02:51):

https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/149/diffs

view this post on Zulip Fabian Kunze (Nov 04 2020 at 08:42):

Also, sometimes using Hint Modes can help: It allow to tell Coq that typeclasses should only be searched if a subset of Parameteres is evar-free by treating them as "input". https://coq.inria.fr/refman/proof-engine/tactics.html#coq:cmdv.hint-mode

view this post on Zulip Paolo Giarrusso (Nov 04 2020 at 12:36):

If you're creating a typeclass you should certainly consider if it needs a Hint Mode.

view this post on Zulip Paolo Giarrusso (Nov 04 2020 at 12:37):

Sometimes, ditto if your libraries create them but have arguably bugs.


Last updated: Feb 01 2023 at 11:04 UTC