<div dir="ltr"><div>Basically what the title says. I've got a goal I'm trying to fill, but the type of the goal is "ModuleName.-invert730 arg1 arg2 ... | someExpr arg1 | someEqProof arg2 ". <br></div><div><br></div><div>If I try to pattern match on "someExpr arg1" I get the dreaded "someExpr arg1 != w" error.</div><div>And if I try to do a rewrite on "someEqProof arg2" I get "lhs != someExpr arg1".</div><div><br></div><div>I'm wondering:</div><div>* Does the -invert autogenerated variable give any hints as to why this is happening? Or is this just normal problems with "with" and "rewrite", and the "-invert" is just an intermediate name that's exposed because evaluation got stuck?</div><div>* Is there any general way to debug/understand what causes the "w !=" or "lhs !=" errors? I'm getting them repeatedly when I work with Agda, and I'd love to actually know what's going on.<br></div><div><br></div><div>I realize it's hard to know what's going on without a minimal example, but the code I've got right now is too big to ask anyone to look at.<br></div></div>