git.iko.soy/Idris-dev
on b3ee2df help sign in
Idris-dev/test/basic009/expected
17 lines 411 B history raw
1MAIN-PASS
2Faulty.idr:6:9-11:num is bound as an implicit
3 Did you mean to refer to A.num?
4Faulty.idr:7:7-12: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:21:import alias not unique: "X"