git.iko.soy/Idris-dev
on d3fa352 help sign in
Idris-dev/test/basic009/expected
17 lines 416 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:When checking right hand side of fault with expected type
5 num = 0
7Type mismatch between
8 0 = 0 (Type of Refl)
9and
10 num = 0 (Expected type)
12Specifically:
13 Type mismatch between
14 0
15 and
16 num
17Multiple.idr:3:1:import alias not unique: "X"