git.iko.soy/Idris-dev
on fd6898e help sign in
Idris-dev/test/basic018/expected
18 lines 484 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:
6When checking right hand side of test with expected type
7 thing = S 41
9Type mismatch between
10 42 = 42 (Type of Refl)
11and
12 thing = 42 (Expected type)
14Specifically:
15 Type mismatch between
16 42
17 and
18 thing