git.iko.soy/Idris-dev
on d689c19 help sign in
Idris-dev/test/tutorial006/expected
37 lines 1.1 kB history raw
1tutorial006a.idr:5:23-24:
2 |
35 | vapp (x :: xs) ys = x :: vapp xs xs -- BROKEN
4 | ~~
5When checking right hand side of vapp with expected type
6 Vect (S len + m) a
8When checking argument xs to constructor Data.Vect.:::
9 Type mismatch between
10 Vect (len + len) a (Type of vapp xs xs)
11 and
12 Vect (plus len m) a (Expected type)
14 Specifically:
15 Type mismatch between
16 plus len len
17 and
18 plus len m
20tutorial006b.idr:10:39-50:
21 |
2210 | parity (S (S (j + j))) | Even = Even {n=S j}
23 | ~~~~~~~~~~~~
24When checking right hand side of with block in Main.parity with expected type
25 Parity (S (S (j + j)))
27Type mismatch between
28 Parity (S j + S j) (Type of Even)
29and
30 Parity (S (S (plus j j))) (Expected type)
32Specifically:
33 Type mismatch between
34 plus (S j) (S j)
35 and
36 S (S (plus j j))