Closed martinescardo closed 2 months ago
And it also type checked fine in previous versions of Agda with --double-check
.
So rather than minimizing the example, it may be more profitable to bisect the Agda code base until we find when the problem is introduced.
This seems to be a reprise of
There is a comment with a workaround that states that the problem already existed with Agda 2.6.3: https://github.com/martinescardo/TypeTopology/blob/02add316f8a78bc79e5687e4249d9f0174dae1d2/source/Naturals/Order.lagda#L76-L91
Closed as duplicate.
I can try to reduce the error later to something self-contained, but for the moment I report this:
This file compiles fine without
--double-check
.