[Agda] rewrite construct not working, when Naturals defined locally?

[David Banas]

I'm finding that code using the *rewrite*-construct works in a file that
imports Naturals, but the same code fails in a different file, which
defines the Naturals locally. In the latter case, expanding the code to its
equivalent *with*-construct form results in successful compilation.

Just wondering if anyone else has observed this, too.

Thanks,
-db
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200816/85845c09/attachment.html>