I find the warnings/error output from agda slightly confusing due to lowercase "when".
To me the lowercase suggests when checking might be continuing from earlier output,
but it seems looking at the source code that when checking actually starts a warning/error message trace.
Personally I would prefer to write it as When checking to make it clearer that starting a warning/error (ie it is about what follows not any preceding lines).
(Of course this might be considered a breaking change since it would be changing the warning/error output format.)
agda-2.6.4 , ghc-9.4.5, Fedora Linux
The issue can be reproduced with the latest version of Agda (either released or master branch).
I have supplied all information so the bug can be easily reproduced (in particular, the reproducer is a complete Agda file).
I am getting warnings/error when building agda-stdlib-{2.7.2,2.7.3} with Agda 2.6.4 (see agda/agda-stdlib#2129 a little context)
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4