git.iko.soy/Idris-dev
on d689c19 help sign in
Idris-dev/test/basic009/expected
32 lines 551 B history raw
1MAIN-PASS
2Faulty.idr:6:9-11:
3 |
46 | fault : num = Z
5 | ~~~
6num is bound as an implicit
7 Did you mean to refer to A.num?
9Faulty.idr:7:9-12:
10 |
117 | fault = Refl
12 | ~~~~
13When checking right hand side of fault with expected type
14 num = 0
16Type mismatch between
17 0 = 0 (Type of Refl)
18and
19 num = 0 (Expected type)
21Specifically:
22 Type mismatch between
23 0
24 and
25 num
27Multiple.idr:3:21:
28 |
293 | import Data.Vect as X
30 | ^
31import alias not unique: "X"