[Agda] What to do when Rewrite fails?

[Nils Anders Danielsson]

On 2020-03-06 21:00, Joey Eremondi wrote:
> I'm wondering, is there a way to manually do the rewrite? The problem
> is that "decEq i i" doesn't actually appear in the type, it's just
> what the evaluation gets stuck on, so I don't think I can use subst.
> Basically, other than rewrite (which is failing), I don't know how to
> tell Agda the value of a term that normalization is stuck on.

If you could show us a (preferably small) self-contained piece of code,
then it might be easier to help you.

-- 
/NAD