Yao Li (Oct 12 2021 at 19:55): Yao Li (Oct 12 2021 at 19:55):I wonder if anyone has any tips on debugging a rewriting does not work with my custom equivalence relation? I have proved the required Proper instance and the instance is in the hint database. When I rewrite Coq says no matching subterms; but an apply would work in the same situation.
Sorry that my question is vague and I don't have a minimal example at the moment. I need to figure out where the problem could be to cut my example to a smaller size...
Paolo Giarrusso (Oct 12 2021 at 20:05):unless you’re trying to rewrite f in f a, I fear the starting point is Set Typeclasses Debug. You could also post a non-minimized example and/or a link to sources, in case somebody can spot something off
Yao Li (Oct 12 2021 at 20:48):Thanks @Paolo Giarrusso! After spending some time eposeing and deciphering the debug info from Set Typeclasses Debug, I find that there is one other relation that I forgot to prove it's an instance of Equivalence. This combined with some issues with implicit arguments led to the issue I had.
Notification Bot (Oct 12 2021 at 21:32):Yao Li has marked this topic as resolved.
Last updated: Oct 13 2024 at 01:02 UTC