Showing content from https://github.com/agda/agda/issues/7262 below:
Error "This clause has target type ... which is not usable" highlights pattern instead of clause · Issue #7262 · agda/agda · GitHub
Skip to content Navigation Menu
Search code, repositories, users, issues, pull requests...
Saved searches Use saved searches to filter your results more quickly
Sign up You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session. You switched accounts on another tab or window. Reload to refresh your session. Dismiss alert
Error "This clause has target type ... which is not usable" highlights pattern instead of clause #7262
Assignees
Description Issue5468.agda:33,7-12 This clause has target type A which is not usable at the required modality @ω.
The correct range would be
33,1-12
.
Currently, attention is directed to a pattern which is not actually the cause of the error.
Metadata Metadata
Development
No branches or pull requests Issue actions
You can’t perform that action at this time.
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