git.iko.soy/Idris-dev
on f0a67ff help sign in
Idris-dev/test/basic009/expected
18 lines 417 B history raw
1MAIN-PASS
2Faulty.idr:6:9-12:WARNING: num is bound as an implicit
3 Did you mean to refer to A.num?
4Faulty.idr:7:7:
5When checking right hand side of fault with expected type
6 num = 0
8Type mismatch between
9 0 = 0 (Type of Refl)
10and
11 num = 0 (Expected type)
13Specifically:
14 Type mismatch between
15 0
16 and
17 num
18Multiple.idr:3:1:import alias not unique: "X"