Shea Levy (Nov 04 2020 at 02:16): 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?
Paolo Giarrusso (Nov 04 2020 at 02:51):https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/149/diffs
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
Paolo Giarrusso (Nov 04 2020 at 12:36):If you're creating a typeclass you should certainly consider if it needs a Hint Mode.
Paolo Giarrusso (Nov 04 2020 at 12:37):Sometimes, ditto if your libraries create them but have arguably bugs.
Last updated: Oct 04 2023 at 23:01 UTC