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
Add a non-existing import to any module. Run idris --check path/to/Module.idr
Expected Behavior
Something that would look like:
Module.idr:3:0-3:10:
|
3 | import Bad
| ~~~~~~~~~~
Can't find import Bad
Observed Behavior
Can't find import Bad
Problem
This problem makes flycheck not work well when importing a non-existing module. Since the output contains no information, flycheck can't point correctly to the line where the problem is.
The text was updated successfully, but these errors were encountered:
Steps to Reproduce
Add a non-existing import to any module. Run
idris --check path/to/Module.idr
Expected Behavior
Something that would look like:
Observed Behavior
Problem
This problem makes flycheck not work well when importing a non-existing module. Since the output contains no information, flycheck can't point correctly to the line where the problem is.
The text was updated successfully, but these errors were encountered: