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
Maybe this is intentional, as the line and column number is still shown.
When I evaluate some code in vs code, I see this:
Errors (1)
/home/brandon/workspace/HaskellAndIdrisNotes/scratch/list_functions.idr:9:21
When checking type of Main.myListRev:
When checking argument y to type constructor =:
Type mismatch between
List a (Type of rev1 a _)
and
Type (Expected type)
Instead of this (from running idris on the file from a terminal):
list_functions.idr:9:21:
|
9 | myListRev: List Nat = rev1 myList
| ^
When checking type of Main.myListRev:
When checking argument y to type constructor =:
Type mismatch between
List a (Type of rev1 a _)
and
Type (Expected type)
The text was updated successfully, but these errors were encountered:
Maybe this is intentional, as the line and column number is still shown.
When I evaluate some code in vs code, I see this:
Instead of this (from running
idris
on the file from a terminal):The text was updated successfully, but these errors were encountered: