git.iko.soy/Idris-dev
on d689c19 help sign in
Idris-dev/test/basic018/expected
32 lines 612 B history raw
1basic018.idr:7:12-16:
2 |
37 | Vect thing elem
4 | ~~~~~
5thing is bound as an implicit
6 Did you mean to refer to Main.thing?
8basic018.idr:12:8-12:
9 |
1012 | test : thing = S 41
11 | ~~~~~
12thing is bound as an implicit
13 Did you mean to refer to Main.thing?
15basic018.idr:13:8-11:
16 |
1713 | test = Refl
18 | ~~~~
19When checking right hand side of test with expected type
20 thing = S 41
22Type mismatch between
23 42 = 42 (Type of Refl)
24and
25 thing = 42 (Expected type)
27Specifically:
28 Type mismatch between
29 42
30 and
31 thing