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