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...
unless you’re trying to rewrite
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
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.
Yao Li has marked this topic as resolved.
Last updated: Jan 29 2023 at 06:02 UTC