On 03/03/2019 13.16, Thorsten Altenkirch wrote: > Otherwise can somebody remind e how to report this? The bug has been reported for you: https://github.com/agda/agda/issues/3604 -- /NAD