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

David Banas capn.freako at gmail.com
Mon Aug 17 17:35:04 CEST 2020


Ah, yes, that was it.
Thank you!
-db


> On Aug 16, 2020, at 10:55 PM, Georgi Lyubenov <godzbanebane at gmail.com> wrote:
> 
> Hi!
> 
> Did you perhaps also redefine equality in the file where it doesn't work, without marking it as BUILTIN?
> 
> =======



More information about the Agda mailing list