lean4-htt/tests/lean/doIssue.lean.expected.out
Markus Himmel eda467e066
fix: typo in application type mismatch error message (#8290)
This PR fixes a typo that was introduced recently.
2025-05-12 13:35:29 +00:00

20 lines
455 B
Text

doIssue.lean:2:2-2:3: error: type mismatch
x
has type
Nat : Type
but is expected to have type
IO PUnit : Type
doIssue.lean:10:2-10:13: error: type mismatch
xs.set! 0 1
has type
Array Nat : Type
but is expected to have type
IO PUnit : Type
doIssue.lean:18:7-18:20: error: Application type mismatch: In the application
pure (xs.set! 0 1)
the final argument
xs.set! 0 1
has type
Array Nat : Type
but is expected to have type
PUnit : Type