git.iko.soy/Idris-dev
on ea745fc help sign in
Idris-dev/test/basic018/expected
17 lines 483 B history raw
1basic018.idr:7:12-17:WARNING: thing is bound as an implicit
2 Did you mean to refer to Main.thing?
3basic018.idr:12:8-13:WARNING: thing is bound as an implicit
4 Did you mean to refer to Main.thing?
5basic018.idr:13:6:When checking right hand side of test with expected type
6 thing = S 41
8Type mismatch between
9 42 = 42 (Type of Refl)
10and
11 thing = 42 (Expected type)
13Specifically:
14 Type mismatch between
15 42
16 and
17 thing