Error "This clause has target type ... which is not usable" highlights pattern instead of clause #7262
Labels
range
type: bug
Issues and pull requests about actual bugs
ux: error reporting
Issues to do with how Agda reports errors
Milestone
agda/test/Fail/Issue5468.err
Lines 1 to 3 in cc78a51
The correct range would be
33,1-12
.Currently, attention is directed to a pattern which is not actually the cause of the error.
The text was updated successfully, but these errors were encountered: