Hi! Did you perhaps also redefine equality in the file where it doesn't work, without marking it as BUILTIN? ======= -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200817/1d002b48/attachment.html>